Parameterized Types

[LighghtEeloo]

This is a proposal for the parameterized type feature, which grants us the ability to define and instantiate a parameterized type with type variables.

An example would be:

data List A where
  | Nil()
  | Cons(A, List A)

This is NOT a proposal about type constructors or polymorphism. All types must be fully instantiated before using.

We should notice that there are two kinds of type variables: value type and computation type. Instead of differentiating them syntactically, we can try to adopt "kind inference" which collects constraints on how the type variables are used, and later assign each of them with a proper kind.

This proposal would also free Thunk and Ret from parser as they should be able to follow the same parsing rules.

[maxsnew]

I would say keep the parentheses required to be consistent with the rest of the language for now (we can talk about dropping them everywhere as a separate issue later):

data List(A) where
  | Nil()
  | Cons(A, List(A))

Also kind inference is good but we should also support annotations, for instance in

data None(A) where

the kind of A is ambiguous.

So what should the syntax for the kinds be? V and C or VTy and CTy or VType and CType or ValueType and ComputationType?

[LighghtEeloo]

I would say keep the parentheses required to be consistent with the rest of the language for now

Noted. I agree.

Also kind inference is good but we should also support annotations

True. I vote for VType and CType as built-in kinds.

[maxsnew]

I'm working on this on a new branch (https://github.com/zydeco-lang/zydeco/tree/parameterized-types)

[maxsnew]

I got stuck on shift-reduce errors. It seems to me that fact that there's so few delimiters in the current syntax makes the grammar very fragile.

[LighghtEeloo]

That's a valid concern to me. One guess is that we can add an end token for declarations and see if it works. Maybe we can somehow share the code that's not working and try to solve it together?

Btw I prefer not to make the syntax layout-sensitive.

[maxsnew]

In implementing this I now realize that this will require some kind of type annotations for comatch statements. For instance the following example can't really be handled by our current type-checker:

codata Fun(a, b) where
| .arg(a) : b
end

(comatch  
  | .arg(x) -> ! exit x
end) .arg(0)

I guess this means some bidirectional stuff?

[maxsnew]

Another example where better checking/synthesis is crucial:

data List(A) where
| Nil()
| Cons(A, List(A))
end

let x = Nil();
...

We won't know what type to give x.

[LighghtEeloo]

Yes, but not completely. This specific example won't run even with the bidirectional type checking shipped in. It will help let bindings, though. For example,

let x : Thunk(Fun(Int, OS)) = {
  comatch
  | .arg(x) -> ! exit x
};
! x

can't type check at the moment without guessing. With bidirectional type checking we can type check this with annotations.

[maxsnew]

Blocked by #32

[LighghtEeloo]

Implemented in #36.