More support for passing types around in the expander

[david-christiansen]

Right now, almost all types (with the exception of annotations using the) are inferred. Even with macrology,the is insufficient, because it only supports ascribing types, rather than type schemes.

Here's a sketch of a design for definition annotations.

Desiderata:

1. Allow partial specification of types/schemes. We don't want to have an all-or-nothing approach, because part of the definition may come from one macro, and part from another. Something like Haskell's PartialTypeSignatures seems much more important here.
2. Respect lexical scoping. A hack like ScopedTypeVariables is not great, because definition forms really bind type variables simultaneously in the equivalent of a System F forall and big-lambda.
3. Don't require large algorithmic changes in the type checker. Right now, the generalization machinery uses the notion of binding levels that I learned from @sestoft rather than scanning the context for free variables, and I'd like to stick with that mechanism for the sake of both efficiency and implementation simplicity.

Here's how I think we can accomplish these goals.

First off, we enrich each syntactic form that's subject to generalization (that is, define, flet, let, and example) with an extra set of parens that binds rigid variables, which we model as fresh type constants in the expander, with an encoding like the one used for names of datatypes. Example syntax in the kernel language:

(define (A) id (the (-> A A) (lambda (x) x)))

We can make this optional in non-kernel languages using a little macro. These bound type variables can only unify with themselves and with metas from their own scope (which means our notion of binding level might need to become a bit more informative, and instead talk about nested scopes rather than just being natural numbers - I'll think about this a bit). When it comes time to generalize, these turn into bound variables from the type scheme. Things to be aware of: 1. rigid type vars that don't get used don't get generalized - so it's "free" to bind a few. 2. unconstrained metas still get generalized, so (define (A) (lambda (x) (lambda (y) (pair (the A x) y)))) will be a (forall (A B) (-> A (-> B (Pair A B)))).

Next, we need a way to provide partial type information to sub-invocations of macros (see @gelisam's talk for the setPartialType operator and its usefulness). I think we can do this with another expression form, with-unknown-type. An expression

(with-unknown-type (M) EXPR)

elaborates EXPR, but with M bound to a new type metavariable. This will allow something like:

(with-unknown-type (A)
  (the (-> (List A) (List A)) (my-macro)))

which lets my-macro do a bit of type-casing without getting blocked. These fresh metas are created at the current binding level, and are subject to generalization from enclosing (but not enclosed) scopes.

We could do something like:

foo :: forall a . a -> _ -> _
foo x y = (x, y)

by expanding to:

(define foo (A)
  (with-unknown-type (B)
    (with-unknown-type (C)
      (the (-> A (-> B C))
        (lambda (x) (lambda (y) (pair x y)))))))

Thoughts?

[langston-barrett]

That all sounds reasonable to me!

[sestoft]

On 3 May 2020, at 00.22, David Thrane Christiansen <[email protected]<mailto:[email protected]>> wrote: Don't require large algorithmic changes in the type checker. Right now, the generalization machinery uses the notion of binding levels that I learned from @sestoft<https://github.com/sestoft> rather than scanning the context for free variables, and I'd like to stick with that mechanism for the sake of both efficiency and implementation simplicity. As far as I know, Didier Rémy devised the “level” mechanism for type variable generalization, see Didier Rémy. Extension of ML type system with a sorted equation theory on types. [Research Report] RR-1766, INRIA. 1992. At https://hal.inria.fr/inria-00077006/document Peter