Expression type annotation vs. Declaration type annotation

[AlexKnauth]

Similar to how : declarations work in Typed Racket or how id :: type declarations work in Haskell, I want to be able to separate definitions from their type annotations like this:

(: f {Integer -> Integer})
(def f (λ [x] x))

I have already implemented most of this (same way as Stephen and I did this in Typed Rosette), but there are some design questions left over.

1. The expression form of type annotation is already called :, and in places where both definitions and expressions are allowed, calling them both : would be ambiguous. The expression version and the declaration version should probably have different names. In Typed Racket the declaration version is : and the expression version is ann, but Hackett might need something different since : is already the expression version.

2. My preliminary implementation of this doesn't include Scoped Type Variables. I have had trouble "communicating" the scope between the type declaration form and the definition form where the scope is needed. We're working on this now. (Edit: now solved.)

[lexi-lambda]

Could you explain why you would want to do this? I’m not immediately sure why that is any more or less readable than the equivalent already available in Hackett:

(def f : {Integer -> Integer}
  (λ [x] x))

[AlexKnauth]

There are two reasons why we want this.

1. Our module system will be easier to implement if this declaration form exists and the inference version of def expands to it. Our module form would recognize it to pull out signature elements from the module body.

2. It puts less text in between an identifier and what it's equal to, making the equations more obvious. This:

fact :: Integer -> Integer
fact 0 = 1
fact n = n * fact (n - 1)

looks just like the set of mathematical equations, but putting a type annotation in between fact and the first 0 obfuscates that a bit. Hackett doesn't quite allow this, but it looks closer with nothing in between the name fact and the first argument pattern.

(: fact {Integer -> Integer})
(defn fact 
  [[0] 1]
  [[n] {n * (fact {n - 1})}])

This looks better to me because it's closer to the equations I would write down in Haskell.

[lexi-lambda]

I understand the sentiment of (2), since it’s “more like Haskell”, and generally, Hackett opts to be like Haskell where possible. That said, I don’t really like the idea. It’s non-local in a way that Racket macros usually aren’t unless they have to be. It also adds two ways to do the same thing, neither of which is ever really better or worse, which I think is normally bad language design.

On the other hand, I think (1) is interesting. Is there perhaps some way that goal could be better served some other way?

[iitalics]

We can almost use the def form for this, however it doesn't work very well for un-annotated definitions, since it just infers then expands into define- and define-syntaxes, which we can't use for modules. We need Hackett to leave behind some sort of syntax that we can examine to determine what bindings the user defined so that we can create module signatures out of them.

[lexi-lambda]

I don’t really understand that much about ML functors, so I’m not entirely sure what you’re doing/need to do, but it seems reasonable to want Hackett to leave behind information after partial expansion. I’ve been thinking it would be good for Hackett to expand into a small, explicitly-typed core language anyway before expanding into untyped Racket, a la GHC’s Core language, so maybe we can make def expand into some kind of Core-def that always includes a type annotation?

[AlexKnauth]

That would be better than the current state of things. The Core-def form would have slightly more information than we would need. All we need is the identifier and the type, not the expression, and that happens to be exactly what a : declaration has. The value parts of a signature could just be the : declarations extracted from a module.