Moreover, there is this Godelian trick to achieve what Haskell achieves with typeclasses + do-notation. Specifically, the do-notation works because the ad hoc polymorphism support in typeclasses allows programmers to provide definitions for unit and bind for a given color of brace. i realized that with a little reflection you can achieve the same thing by making the color of a given brace be the term that implements unit and mult-or-bind.

Below is a little BNFC code which will generate Haskell data types and a parser for the term language.

Application . Term ::= "(" Term [Term] ")" ;

Abstraction . Term ::= "lambda" [Variable] "." Term ;

Reference . Term ::= Variable ;

Zero . Term ::= "0" ;

Embracing . Term ::= Embrace ;

Quotation . Variable ::= "@" "{" Term "}" ;

Variation . Variable ::= Ident ;

Unity . Embrace ::= "{" Color "|" Term "|" Color "}" ;

Multiplicity . Embrace ::= "*" "{" Color "|" Embrace "|" Color "}";

Interchange . Embrace ::= "~" "{" Color "|" Embrace "|" Color "}";

Coloring . Color ::= Variable ;

[] . [Variable] ::= ;

(:). [Variable] ::= Variable [Variable] ;

[]. [Term] ::= ;

(:). [Term] ::= Term [Term];

i'm going to have to do the detailed unpacking a little later as i'm getting hungry... But, these are the essential elements of the approach.

- Use the idea of injecting the λ-calculus into a term language for monad expressions
- The term language of expressions is essentially
- unit for the monad associated to color k is written: {k| t |k}
- mult for the monad associated to color k is written: *{k| {k| t |k} |k}
- and, because we want to demand distributivity over our monads we ask for an interchange expression #{j| {k| t |k} |j}

- Finally, we use terms themselves as colors, k.

## No comments:

Post a Comment