Add a "syntax AST" for typedefs

[andrevidela]

All #133 #164 #163 #172 require changes to the AST but do not necessarily change the semantics of the language. This means it would be possible to write a new syntax for typedefs that compiles down to TDef n and that is more ergonomic and feature rich than our core AST TDef n.

Here is a small proposal for a new surface level syntax

bool := 1 + 1

maybe a := nothing := 1 + just := a

either a b := left := a + right := b

eitherAnon a b := a + b

byte := bool ^ 8

list a := nil := 1 + cons := a * list a

this would compile down to

(name bool (+ 1 1))

(name maybe (mu (nothing 1) (just (var 1))))

(name either (mu (left (var 1)) (right (var 2)))

(name eitherAnon (+ (var 0) (var 1)))

(name byte (* (ref bool) (ref bool) (ref bool) (ref bool) (ref bool) (ref bool) (ref bool) (ref bool)))

This would allow us to add new features to typedefs without having to change backends and making sure the semantics of the language are never changed.

I've added a branch which implement this syntax as an EDSL (without the conversion to TDef) here: https://github.com/typedefs/typedefs/tree/surface-syntax the relevant file is src/DSL.idr

This feature would also fix #23

Could you please tell me what you think @clayrat @fredrikNordvallForsberg @wires @epost ?

[epost]

Note: this syntax is mu-free; those should be implicit.

[fredrikNordvallForsberg]

Looks nice, especially with the translation from recursive definitions to explicit mus. This is clearly needed for wider adoption of Typedefs in the long run.

Some bikeshedding:

• Personally I think reusing := both for named definitions and types of constructors is confusing, especially when associativity is unclear (e.g. a := b := c). How about simply : for the type of constructors (e.g. a := b : c).
• Similarly, reusing + to separate the different constructors also seems confusing to me (e.g. compare a := b := c + d with a := b := c + d := e). How about using | instead (e.g. (with the previous item also taken into account) a := b : c + d and a := b : c | d : e)?

[andrevidela]

@fredrikNordvallForsberg Your comments make sense, I'll try updating the example so we can see how it looks like.

I currently have no intuition about how to compile recursive types defintions into TMus, for example

Tree e := Leaf : 1 | Branch : e * Tree e * Tree e

This should compile to

(name Tree (mu (Leaf 1)
               (Branch (* (var 1) (var 0) (var 0)
                       )
               )
           )
)

Is it correct to replace every recursive definition by (var 0) and stick a mu at the top level?

[andrevidela]

I've implemented your syntax @fredrikNordvallForsberg at 891c074

I couldn't use | as an operator so I implemented || instead, but the show function shows |. Tell me how it looks.

I was considering replacing * by , but it starts to look a bit strange, see

List a := 1 | a , List 1

instead of

List a := 1 | a * List 1

[fredrikNordvallForsberg]

Is it correct to replace every recursive definition by (var 0) and stick a mu at the top level?

As a first approximation yes, but there is a subtlety with nested mus: every time you go under another mu, you need to shift the index of the variable being substituted in by one.

[fredrikNordvallForsberg]

I've implemented your syntax @fredrikNordvallForsberg at 891c074

That looks better, in my opinion. However I think it would still make sense to keep + for representing TSum?

[andrevidela]

@fredrikNordvallForsberg Do you have an example of a recursive definition that compiles to two nested TMu and with a free type variable? I tried to come up with something but my examples don't really work.

Regarding + and | the fact that we have both is just an artifact of me reusing the Num interface for the sake of the prototype. I don't think we should have both syntax in the language. I mean It depends what we want to achieve with the language but as a general rule I don't think it's often beneficial to have multiple ways of achieving the same thing, specially when regarding syntax.

Unless we want to enforce | when separating named constructors and + when using anonymous unions. That would make the grammar a bit more complicated but may be worth exploring

[fredrikNordvallForsberg]

Do you have an example of a recursive definition that compiles to two nested TMu and with a free type variable?

A common example is finitarily branching trees (with data at the leaves, say):

Tree a := Leaf : a | Node : List (Tree a)

which (if we keep the list anonymous) should compile to

treeDef : TDef 1
treeDef = TMu [("Leaf", var 1),
               ("Node", TMu [("Nil", T1),
                             ("Cons", TProd [var 1, var 0])])]

unless I have messed up. The Leaf var 1 refers to the type variable, The Cons var 1 refers to the recursive reference to Tree, and the var 0 refers to the most local mu, e.g. to the list.

Unless we want to enforce | when separating name constructors and + when using anonymous unions.

Yes, that's what I had in mind, sorry if I was unclear!

[andrevidela]

So I tried to retrofit your example into the proposed syntax but since sums involving constructors are automatically converted into a TMu with no scoping rules there is no way to inline the definition of list. It's the same as you've written:

List a := Nil : 1 | Cons : a + List a

Tree a := Leaf : 1 | Node : List (Tree a)

This makes your proposal of having | for constructors a lot stronger since now we can say that every | compiles to a top-level TMu and you can't nest |