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

mafm

Keybase proof

I hereby claim:

• I am mafm on github.
• I am mafm (https://keybase.io/mafm) on keybase.
• I have a public key whose fingerprint is E400 C3AC EC79 56C3 D6FE 927A FA3B 8B70 4B38 F927

To claim this, I am signing this object: