The following appears to be an adequate encoding of the untyped lambda calculus in Standard ML:
datatype ('a,'b) term = T of
('b -> 'a)
* ('a * 'a -> 'a)
* (('a,('b option)) term -> 'a)
-> 'a
datatype void = V of void
type 'a tm = ('a, void) term
Every value at type 'a tm should correspond to an untyped lambda term.
datatype ('a,'b) term = T of
('b -> 'a)
* ('a * 'a -> 'a)
* (('a,('b option)) term -> 'a)
-> 'a
datatype void = V of void
type 'a tm = ('a, void) term
Every value at type 'a tm should correspond to an untyped lambda term.