49

I've been reading up on various type systems and lambda calculi, and i see that all of the typed lambda calculi in the lambda cube are strongly normalizing rather than Turing equivalent. This includes System F, the simply typed lambda calculus plus polymorphism.

This leads me to the following questions, for which I've been unable to find any comprehensible answer:

  • How does the formalism of (e.g.) Haskell differ from the calculus on which it is ostensibly based?
  • What language features in Haskell don't fall within System F formalism?
  • What's the minimum change necessary to allow Turing complete computation?

Thank you so much to whomever helps me understand this.

JwameeQohwiye
  • 603
  • 5
  • 6
  • 10
    Haskell's Core calculus isn't strongly normalizing. It's a superset of System-F that includes recursive bindings which allows recursion. – Stephen Diehl Aug 12 '14 at 03:09
  • Also note that Haskell is (to my understanding) descended from ML, rather than System F. So there's a generation in between that took the biggest leap. – Patrick Collins Aug 12 '14 at 03:45
  • 1
    @PatrickCollins The Hindley-Milner system used in ML is *weaker* than System F. So without recursion it's still normalizing. With added recursion they are both TC. – Ørjan Johansen Aug 12 '14 at 09:07
  • See also http://cs.stackexchange.com/questions/2638/does-there-exist-a-turing-complete-typed-lambda-calculus and http://cstheory.stackexchange.com/questions/29519/what-functions-can-system-f-not-compute – ziggurism Nov 17 '15 at 04:23

1 Answers1

54

In a word, general recursion.

Haskell allows for arbitrary recursion while System F has no form of recursion. The lack of infinite types means fix isn't expressible as a closed term.

There is no primitive notion of names and recursion. In fact, pure System F has no notion of any such thing as definitions!

So in Haskell this single definition is what adds turing completeness

fix :: (a -> a) -> a
fix f = let x = f x in x

Really this function is indicative of a more general idea, by having fully recursive bindings, we get turing completeness. Notice that this applies to types, not just values.

data Rec a = Rec {unrec :: Rec a -> a}

y :: (a -> a) -> a
y f = u (Rec u)
  where u x = f $ unrec x x

With infinite types we can write the Y combinator (modulo some unfolding) and through it general recursion!

In pure System F, we often have some informal notion of definitions, but these are simply shorthands that are to be mentally inlined fully. This isn't possible in Haskell as this would create infinite terms.

The kernel of Haskell terms without any notion of let, where or = is strongly normalizing, since we don't have infinite types. Even this core term calculus isn't really System F. System F has "big lambdas" or type abstraction. The full term for id in System F is

id := /\ A -> \(x : A) -> x

This is because type inference for System F is undecidable! We explicitly notate wherever and whenever we expect polymorphism. In Haskell such a property would be annoying, so we limit the power of Haskell. In particular, we never infer a polymorphic type for a Haskell lambda argument without annotation (terms and conditions may apply). This is why in ML and Haskell

let x = exp in foo

isn't the same as

(\x -> foo) exp

even when exp isn't recursive! This is the crux of HM type inference and algorithm W, called "let generalization".

daniel gratzer
  • 52,833
  • 11
  • 94
  • 134
  • 5
    Note that recursive types like Haskell offers also imply general recursion. – Dominique Devriese Aug 12 '14 at 04:31
  • @DominiqueDevriese Would inductive or co-inductive types also be equivalent to general recursion? – JwameeQohwiye Aug 12 '14 at 13:58
  • @DominiqueDevriese Am I right in guessing that coinductive types allow general recursion, while inductive types don't? – JwameeQohwiye Aug 12 '14 at 14:06
  • I don't think that either inductive or coinductive types necessarily allow general recursion. For example, Coq and Agda have both but they are total. Note that e.g. inductively defined types are subject to certain restrictions (e.g. strict positivity) precisely to ensure this. – Dominique Devriese Aug 13 '14 at 06:50
  • Disagree. Almost. You have explained a *symptom* but not the cause; The *cause* that makes general recursion possible is both a lack of totality checking and a lazy runtime. Totality checking would barf on such forms of recursion leaving you without turing completeness - so the lack of Haskell's totality checking is one necessity. Though even without totality checking, an eager runtime would barf on Haskell's recursion. So the combination of those two artifacts allow the recursion and turing completeness you refer to. (I think.....) – Jimmy Hoffa Aug 13 '14 at 21:49
  • 2
    @JimmyHoffa Totality checking is necessary when you have recursive binding but want to act as though those bindings can only do folds on data and unfolds on codata. If you just don't (or do) introduce either value- or type-level `fix` then you automatically get completeness. – J. Abrahamson Aug 22 '14 at 00:48
  • 4
    @JwameeQohwiye Neither inductive types, coinductive types, or the combination is powerful enough to get completeness. It's only if you can pass from codata to data or visa versa. – J. Abrahamson Aug 22 '14 at 00:49
  • What do you mean by `fix :: (a -> a) -> a`, since `fix` shouldn't be typable? – Couchy Aug 07 '20 at 11:01