Closed dougalm closed 1 year ago
Type constructor application and data constructor application should probably look the same as function application. I don't mind f(x, y) but I don't love the look of Maybe(Float) and Just(1.2). But I'd probably get used to it.
Rust seemingly hews close to Haskell syntax and adds parens. (Not sure if good or bad):
https://serokell.io/blog/rust-vs-haskell#option-%2F-maybe-and-result-%2F-either
I think you are describing Scala! ;-) But seriously, if you are thinking about going down this route, you should take a very careful look at Scala's approach to type syntax, type signatures, partial application, named and default arguments, and currying. And regarding multi-line continuations, you will probably be interested in the optional braceless (whitespace significant) syntax of Scala 3, which is proving controversial, but I like.
I'm overall in favor of stopping currying - every time I use it I feel like I'm setting the reader up for confusion. It also took me a little while to begin to automatically look for arity errors when I saw type errors.
Regarding named optional arguments, I've usually been able to use the type system to implicitly specify them, but sometimes it's a bit awkward, especially at the top level. I wonder if we could further reduce the distinction between explicit and implicit arguments. E.g. if there is only one valid variable of each argument type in scope that could be used by a function, allow a syntax like f( _ )
or f( x=y, ... )
to fill in all the (remaining) blanks at once.
@srush , thanks for the link to that Rust<->Haskell writeup. It helps to see things side-by-side like that. We should do the same thing for Dex some time.
I think you are describing Scala! ;-)
If so, great! If we can avoid having to reinvent concrete syntax then all the better. Do you have any syntax references for Scala you recommend? Is "generic class" the right Scala concept for what we call algebraic data types in Haskell? It looks like Scala uses square brackets for type parameters, like List[A]
. In Dex we probably want to use the same notation for type application and ordinary term application.
I really enjoy working with curried functions. I would be interested though in "More Flexible Partial Application".
To expand on this, since toying around with haskel, dex and agda over the past year, I found that expressing functions in their curried form can often make the math "clearer".
Also -->
Some random facts that might be relevant.
Core
for OCaml, function like map
has type
val map : 'a list -> f:('a -> 'b) -> 'b list
rather than the more familiar (Haskell, vanilla OCaml etc.)
map : (a -> b) -> [a] -> [b]
So when f
spans multiple lines, it looks better:
let v = List.map some_list ~f:(fun x ->
...)
More motivations regarding this design choice and some suggestions can be found here.
Done, #1250
Idiomatic Dex, like Haskell, uses curried unary functions rather than explicit n-ary functions. When you write
f x y
it parses and behaves as(f x) y
. The neat thing about this style is that it makes partial application easy, so you can write things likeadd_one_to_each = map (add 1.0)
. Pretty cool! But maybe it's just a party trick? It definitely comes with some costs and we're not the first to wonder if it's a net win.How would things improve if we moved to explicit n-ary functions?
Better arity error messages
If we provide too few arguments to a function we get this:
And if we provide too many:
Not great! If there's some polymorphism involved, it gets even worse:
Compare that to e.g. Python:
Better call stack traces
We want to give call stack traces for runtime errors. These are easier to interpret with explicit n-ary functions than with curried unary functions where only the innermost lambda (which doesn't even have a name) provides a stack frame.
Named optional arguments
N-ary application syntax enables named arguments, and named arguments enable optional arguments. We currently have implicit arguments, like
a
andb
inswap : (a:Type) ?-> (b:Type) ?-> (a, b) -> (b, a)
but there's no way to providea
andb
explicitly. We could adopt Haskell's@
syntax but that still doesn't give us a way to provideb
explicitly without providinga
. Named arguments solve the problem neatly, with application syntax likeswap(b=Nat, 1 2)
.More flexible partial application
Currying is great for partial application, but only if it's the first argument(s) that you want to partially apply. Otherwise you have to use
swap
or explicitly eta expand. This has a funny effect on the library ecosystem: when we define a function, we tend to look at the arguments that we might want to "freeze" (i.e. partially apply) and then we put those first. These are often "configuration" flags rather than the data objects of interest. This leads to the opposite convention from what we see in other languages, where configuration arguments tend to go at the end, often as optional arguments.Explicit n-ary application makes it harder to partially apply the first argument, but it opens the door to partial application syntax that makes it possible to partially apply any argument. We can imagine something like
f(x, y, _)
being syntactic sugar for\z. f(x, y, z)
. (Though we can't actually use_
because it already means mean "compiler, please fill this in for me". What's better??
?,*
?,.
?)Implementation convenience
We work with explicit n-ary functions internally, from SimpIR onward. There's a lot of hassle in converting back and forwards between the user-facing curried form and the internal uncurried form.
Design question: polymorphic data
Consider the identity monoid element. In current Dex it's a binary function:
But both arguments are implicit, so you "call" it by just mentioning it. But in a world with n-ary functions there's a difference between mentioning a function and calling it with zero arguments. So would we have to write
mempty()
? Maybe that's not a bad thing? Implicit functions likemempty
unintentionally doing work are the reason for the "dreaded monomorphism restriction". Maybe we're actually better off making it more syntactically obvious that they're functions.Design question: parens or no parens?
N-ary function application is traditionally written as
f(x, y)
. But we could ignore that and keep using juxtaposition, parsingf x y
asApp f [x, y]
. (If you really wantedApp (App f [x]) [y]
you'd write((f x) y) z
instead.)Some quick observations
Arguments in favor of
f(x, y, z)
f()
f(x=1, y=2)
looks easy to parse, whereas withf (x=1) (y=2)
you have to consider that(x=1)
might be an expression.Arguments in favor of
f x y z
f(x, y)
but I don't love the look ofMaybe(Float)
andJust(1.2)
. But I'd probably get used to it.with_state 1.0 \ref . ...
. That becomes a problem with parenthesized application because the closing paren belongs several lines down. But perhaps this pattern is common enough to deserve its own syntax anyway. As with the earlier point about curried partial application encouraging you to write functions with flag arguments first, the trailing continuation pattern encourages you to write functions with the continuation last. Maybe instead we can have some special syntax for writing multi-line lambda terms as arguments and then the continuation argument can be in any positions. And maybe you can even have more than one of them, like you'd want for a user-levelCase
combinator.