search

Toxaris / pts

Interpreter for functional pure type systems.
BSD 3-Clause "New" or "Revised" License
21 stars 7 forks source link

Integrate with SugarJ #44

Open Toxaris opened 11 years ago

Toxaris commented 11 years ago

Integrate with the SugarFOmega variant of SugarJ in order to create SugarPTS.

See seba--/sugarj and florenzen/sugarj.

Blaisorblade commented 11 years ago

You wrote in https://github.com/Toxaris/pts/issues/49#issuecomment-15199660:

If I understand correctly, SugarFω natively supports products, sums, and iso-recursive types. Datatype syntax à la Haskell or ML is provided as syntactic sugar on top of that.

I also wondered whether iso-recursive types (and the rest) could be syntactic sugar on top of Church-encoding, but that's not obvious. In Pierce's book, iso-recursive types allow for non-termination, at least because of recursion in contravariant positions; moreover, Haskell/ML ADTs (which require unrestricted recursion) are more expressive than Church-encoded values, and probably equi-expressive to Scott-encoded types (which require fixpoints anyway).

But maybe we still want to implement fixpoints anyway (as an extra option), don't we? In the "trying out things" spirit, that'd make sense.

Toxaris commented 11 years ago

I agree that we currently cannot encode full algebraic data types. Some details: Böhm and Berarducci (1985) show how to adequately Church-encode strictly positive algebraic data types. We can also support some positive function spaces using the techniques of Washburn and Weirich (2003). I don't think we can support negative function spaces. My intuition for this is: Church-encoding is about enumerating all constructors, so it only works for data, not for codata, and certainly not for the data-mixed-with-codata provided by Haskell algebraic data types.

References:

Corrado Boehm and Alessandro Berarducci (1985). Automatic Synthesis of Typed Lambda-Programs on Term Algebras. Theoretical Computer Science 39: 135-154

Geoffrey Washburn and Stephanie Weirich (2003). Boxes go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism. In Proceedings of ICFP.

Blaisorblade commented 11 years ago

I agree that we cannot support full algebraic data types.

I hope that there you're not excluding the "fix" instance feature, and (EDIT) you're just describing what we can do without fixpoints.

Toxaris commented 11 years ago

I edited my comment to clarify what I mean: With the current implementation, we cannot encode full algebraic data types. By adding enough features, we could certainly build a language that can encode them.