Integrate with SugarJ

[Toxaris]

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

See seba--/sugarj and florenzen/sugarj.

[Blaisorblade]

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]

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]

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]

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.