# Lexical Data - Lexical Scoping is a Right, Not a Privilege

## February 20, 2014

I had an interesting conversation with Edward Amsden yesterday. The crux of it was his claim that modern functional languages do an incredibly poor job of scoping data definitions. By comparison, languages like Scheme, ML, and Haskell can easily and cleanly scope any value you give it through let and lambda. And the variables bound by these forms don’t have a large scope or a long life time: they don’t live as a top-level definition. So why do ADTs?

The language Idris introduces name spaces, which help ease the problem, but they still require programmers to define data types in a namespace-global way:

It’s interesting, though. If I would like to define an interpreter of type Exp -> Val which implicitly uses some environment to find the result without wishing to expose it to the user, I can easily write the full version inside in even Haskell:

And yet, the environment here must still be exposed in the global namespace of the local module:

This is globally exposed: not only does interpH use it, but any other piece of code is free to use this environment definition anywhere in the module. The philosophical argument behind functional programming that that functions are first-class values. So why do we insist that functions should get this treatment, but data-type declarations do not?

That’s the crux: why can’t I also define lexically-scoped data, close to the way I can define lexically-scoped helper functions? Ideally, I’d like to write this code:

I want the entire type of Env lexically enclosed, just like helper functions are. And further, I’d like for every definition to get such treatment. Even type-class instances should get this! If it’d like, I should be able to write this code:

It’s the case that Idris does support this, quite nicely. (David Christiansen has provided this code.)

It’s likely this works in Agda, too. And this is important; data definitions should be subject lexical scoping. Why should functions get preferential treatment?

### Using LaTeX for Programming Language Semantics

LaTex is a fantastic tool for typesetting, but there seem to be a serious gapin documentation for using it to lay out programming semanti...… Continue reading

#### A Small ALU in Haskell, Part I

Published on April 24, 2015

#### The Refined Gradual Guarantee and Compilation

Published on April 15, 2015