Constructors / bidirectional pattern synonyms

[byorgey]

Currently we can define ADTs using recursive sum types, e.g.

type Tree = Unit + N * Tree * Tree

We can then define constructor synonyms like

leaf : Tree
leaf = left ()

node : N -> Tree -> Tree -> Tree
node x l r = right (x,l,r)

but these can only be used to construct Tree values, not to destruct them. i.e. when pattern matching on a Tree value we have to match on left/right; we can't match on leaf/node. It would be cool to be able to specify that leaf and node are constructors, and have the system check that their definitions are also valid patterns. This shouldn't be too hard now that we actually process patterns as special terms anyway. So something like

constructor leaf : Tree
leaf = left ()

constructor node : N -> Tree -> Tree -> Tree
node x l r = right (x,l,r)

root : Tree -> N
root leaf = 0
root (node x _ _) = x

This is not a high priority, and pedagogically one might not want to introduce this feature, but it would be cool anyway and probably (?) not too hard to implement.

[byorgey]

Really this isn't about constructors in particular but pattern synonyms in general. But I think we want to only allow simple bidirectional pattern synonyms, and "constructor" is still a good name for such things. Here's a general outline of a design:

• When parsing, if we notice the keyword constructor before a type declaration, parse it as a normal type declaration but store a flag denoting that it is a constructor.
• When type checking a definition of a thing flagged as a constructor, ensure that (1) it has only a single clause, and (2) the term on the RHS of that clause is also a valid pattern.
• We need to add another (Haskell) constructor in the pattern AST type to denote (Disco) constructors.
• Extend the termToPattern function to allow application, as long as the thing on the left is a constructor. Also, when encountering a variable, we must check to see if it is a constructor name in scope to decide whether to turn it into a constructor pattern or a normal PVar pattern.
• When matching a pattern, look up encountered constructors and match on their definition appropriately.

[byorgey]

I was thinking that it would be nice to implement this so we can e.g. implement Bool in a library, instead of having it built in. e.g.

type Bool = Unit + Unit
constructor false : Bool
false = inl(unit)
constructor true : Bool
true = inr(unit)

However, the big problem is that we want Bool values to also be pretty-printed as false and true. This is a bit more complicated, but perhaps it's possible. The idea would be that for a given type, we classify ahead of time the possible values of that type and how they map onto the different possible constructors.

[byorgey]

I have thought more about the above comment and am now convinced that it is possible in a principled way:

• Constructor patterns can be translated away during desugaring.
• To each user-defined type, associate a list of constructor names with their pattern definition (i.e. those constructors which result in the given type).
• During pretty-printing, when pretty-printing a value of a user-defined type, try matching the value against each associated constructor pattern of that type. Pick the first matching one and pretty-print using that constructor.

All of this would become much easier once Disco is eager and we don't have to interleave pretty-printing and evaluation. Note applications of delay will just be pretty-printed as ... or something like that; pretty-printing will not force evaluation at all.

[byorgey]

Note that implementing Bool in a library also requires #136 .

[byorgey]

Note that case expressions {? ... ?} are built-in notation that rely on Bool. However, if Bool was not built-in, I think we could do something similar to what e.g. Coq does (if I remember correctly): expressions are considered "truthy" or "falsy" simply depending on whether they use a left or right constructor.

Ultimately, though, I'm not sure it's worth it to have Bool defined in a library.

[byorgey]

Reading this over again, I think we definitely don't want Bool defined in a library. This whole issue is pretty low-priority but could be a fun issue for a student or other new contributor to tackle.