dex-lang
dex-lang copied to clipboard
google-research
Harmonize syntax of functions, arrays, and function types
[This grew out of thinking about #925.]
Right now, there is a disharmony in Dex syntax. From Haskell, we write function types separating every argument's type with an arrow:
n:Type ?-> Ix n ?=> x:Float -> n => Float
By analogy with functions, we write array types separating every index with an arrow:
i:(Fin 20) => i => Float
However, from Python, when defining a function with def, we write the arguments, and their types, separated from each other with whitespace and from the result with :, thus:
def foo {n} [Ix n] (x:Float) : n => Float = ...
Without the arrows to tell us what kind of argument each argument is, we use brackets.
Likewise, from both Haskell and Python, when defining an anonymous function with \, we write the arguments separated from each other with whitespace, and from the body with a .. (But, idiosyncratically, lambda binders allow type annotations.)
This state of affairs registers to me as pretty unfortunate. Function types don't look like the syntax for defining them. That makes it more difficult to mentally translate a type to a definition or vice versa. It also impedes copy-paste from one form into the other because of the large post-paste edit distance. And there's very little structural reason to make them different, because both forms introduce binders, which even have essentially the same scope!
I've been thinking about harmonzing by making function types look like function definitions. I don't think there's any clean way to parse juxtaposition as "several arguments to a function type" without introducing a leading disambiguator. I was thinking of introducing a new fun or funty keyword, but then it occurred to me that we can reuse lambda, with a different result delimiter. For example,
\{n} [Ix n] Float -> n => Float
(note the -> arrow instead of .) could parse as the type currently spelled n:Type ?-> Ix n ?=> x:Float -> n => Float. We could also take a leaf out of Clojure's book and say fn instead of \ in both cases.
However, that change syntactically obscures the analogy between functions and arrays. How much do we value that analogy? Do we want to (re-) introduce arrows into def syntax to harmonize across all three? Then we could write
def foo {n} -> [Ix n] -> (x:Float) -> n => Float = ...
and
{n} -> [Ix n] -> x:Float -> n => Float
for a definition and its type, respectively, keeping array types as they are. But did we not already change def away from this style? Presumably it was found to be annoying?
Or we could change array types to take all their indices whitespace-separated as well, to harmonize them with functions:
arr (i:(Fin 20)) i => Float
We could even go so far as to pun the for keyword for this, as
for (i:(Fin 20)) i => Float
(disambiguating against loops by writing => instead of .)
One down side of this last approach is that it obscures the chained-indexing nature of arrays; i.e., it becomes somewhat unintuitive that an object of type arr (i:(Fin 20)) i => Float can be indexed with one index of type Fin 20 to produce a one-dimensional array. For functions this is I think less of an issue because application is whitespace, so there's already a syntactic pun between f a b c and ((f a) b) c.
Thoughts?
Nitpicks:
- Regardless of the larger change, I think it would be nice to use the same token (either
->or:) for the result of a function regardless of whether it appears in a type or in a definition. - Since the body of a
defis already delimited by=, we can make the result annotation optional, defaulting to: _, asdef id (a:Float) = a. - Conversely, we could allow annotating the result type (as well as the effects) of an anonymous function (since we allow annotating the binders), with a syntax like
\{n} [Ix n] Float -> n => Float . <body>. - Speaking of which, how much do we actually want to pattern-match singleton tables in lambda arguments? Why not just say that's not allowed because it conflicts with the syntax for annotating constraints, and make the user unpack any such things in a let binding in the body of the lambda?
- If we change the delimiter for "this is the result type" from
:to something else (like->), we may be able to make the parens around explicit arguments optional. We can also make their type annotations optional, letting the user writedef id a = afordef id (a:_) : _ = a(though maybeidis the only function that can actually be written like this?)