I want to implement an example which demonstrates that it is possible to define a #lang with a custom type system. More specifically, I want a type system which, as Conor McBride exhorts, does more than just rejecting bad programs, and in addition generates terms.
My current plan is to implement Scala's "implicit conversion" feature. That is, a function from A to B can be added to the list of implicit conversion functions currently in scope, and then if within that scope an A is used where a B is expected, the conversion function is automatically inserted. Here is some example code I am hoping to support:
Since my goal is only to demonstrate that this is possible, not to use the #lang in anger, I only plan to implement the minimum set of functionality to support the above example. In particular, I am not planning to include lambdas in the #lang.
I want to implement an example which demonstrates that it is possible to define a
#lang
with a custom type system. More specifically, I want a type system which, as Conor McBride exhorts, does more than just rejecting bad programs, and in addition generates terms.My current plan is to implement Scala's "implicit conversion" feature. That is, a function from
A
toB
can be added to the list of implicit conversion functions currently in scope, and then if within that scope anA
is used where aB
is expected, the conversion function is automatically inserted. Here is some example code I am hoping to support:Which would become
Since my goal is only to demonstrate that this is possible, not to use the
#lang
in anger, I only plan to implement the minimum set of functionality to support the above example. In particular, I am not planning to include lambdas in the#lang
.