Not quite. You're appleaing to the Curry-Howard correspondance, which is neat but is not used by many theorem provers. Furthermore, > fun fix (f : 'a -> 'a

Not quite. You're appleaing to the Curry-Howard correspondance, which is neat but is not used by many theorem provers. Furthermore, > fun fix (f : 'a -> 'a) : 'a = fix f; val fix = fn: ('a -> 'a) -> 'a The trick is that all functions must be total, which is the crux of the matter (and why the Y-combinator exhibits the paradox, because it allows nontermination). This is why we have stuff like the polymorphic lambda calculus, in which termination is guaranteed and the Y-combinator is untypeable.