mafm

from __future__ import unicode_literals
import sys

# We only use unicode in our parser, except for __repr__, which must return str.
if sys.version_info.major == 2:
    repr_str = lambda s: s.encode("utf-8")
    str = unicode
else:
    repr_str = lambda s: s

mafm

(* This is a demonstration of the use of the SML module system to
   encode (Generalized Algebraic Datatypes) GADTs via Church
   encodings. The basic idea is to use the Church encoding of GADTs in
   System Fomega and translate the System Fomega type into the module
   system. As I demonstrate below, this allows things like the
   singleton type of booleans, and the equality type, to be
   represented.

   This was inspired by Jon Sterling's blog post about encoding proofs
   in the SML module system:

mafm