A type signature in Haskell is written in the following format:

functionName :: arg1Type -> arg2Type -> returnType

There's a (hyphenated, after a person or persons) name for this style of type signature (which predates Haskell), but it's escaping me and I can't find it anywhere.

  • 2
    $\begingroup$ This style of definition isn't really due to Haskell is it? It's existed in type theory (70s and earlier) which led to languages inspiring Haskell and far before that it existed in the mathematical community at large. $\endgroup$ – Daniel Gratzer Jan 6 '16 at 19:19
  • $\begingroup$ Yes, correct -- it's not exclusive to Haskell. I'll make this clear. $\endgroup$ – Jake Romer Jan 6 '16 at 19:20
  • $\begingroup$ I'd look into the origins of ML Syntax, I think it likely originates from there (though it's possible it can be traced earlier back). $\endgroup$ – jmite Jan 6 '16 at 23:17
  • 2
    $\begingroup$ By the way: in Haskell, and in several other FP languages, it's more common to find curried functions/signatures f :: arg1Type -> arg2Type -> returnType instead. $\endgroup$ – chi Jan 7 '16 at 19:07
  • $\begingroup$ Do you mean Church-style (as opposed to Curry-style) for lambda calculus, i.e. type checking only instead of type inference? $\endgroup$ – Cactus Jan 8 '16 at 6:04

Is it Hindley-Milner type system by any chance?

| cite | improve this answer | |
  • 1
    $\begingroup$ Could be what the original poster was thinking of, but I don't believe the Hindley-Milner type system is a name for the notation for writing function type signatures. HM is the algorithm / type system for doing type inference (inferring polymorphic type signatures), not the notation for how to write the type signature. (I suspect I'm saying things you already know.) $\endgroup$ – D.W. Jan 7 '16 at 8:49
  • 1
    $\begingroup$ Sure, I think we have a case of someone who is not really a programming languages person, so the question should be understood broadly. In any case, the OP will hopefully react. $\endgroup$ – Andrej Bauer Jan 7 '16 at 9:07
  • $\begingroup$ As Phil Wadler famously noted, Curry-Howard is the double-barreled name that predicts other double-barreled names (e.g. Hindley-Milner, Girard-Reynolds, though not Martin-Löf). $\endgroup$ – Pseudonym Mar 7 '19 at 5:34
  • $\begingroup$ Yeaj, but we might as well count Martin-Löf as two. $\endgroup$ – Andrej Bauer Mar 7 '19 at 7:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.