Stack Overflow
Stack Overflow

Questions tagged [hindley-milner]

In type theory, Hindley–Milner (HM) is a classical type inference method with parametric polymorphism for the lambda calculus.

In , Hindley–Milner (HM) is a classical type method with for the lambda calculus.

One property that makes the Hindley-Milner type theory important is its completeness and its ability to deduce the most general type of a given source without the need of any type annotations or other hints. HM is a fast algorithm that can compute a type almost in linear time with respect to the size of the source, which makes it of practical use for the types of large programs. HM is used for several functional programming languages. It was first implemented as part of the type system of the programming language . Since then, HM has been extended in various ways, most notably by constrained types as used in , which it has a strong association with.

The original paper

A Theory of Type Polymorphism in Programming

Languages implementing Hindley-Milner

See also

84 questions
925
votes
6 answers

What part of Hindley-Milner do you not understand?

I swear there used to be a T-shirt for sale featuring the immortal words: What part of do you not understand? In my case, the answer would be... all of it! In particular, I often see notation like this in Haskell papers, but I have no clue what…
MathematicalOrchid
  • 61,854
  • 19
  • 123
  • 220
146
votes
3 answers

What is Hindley-Milner?

I encountered this term Hindley-Milner, and I'm not sure if grasp what it means. I've read the following posts: Steve Yegge - Dynamic Languages Strike Back Steve Yegge - The Pinocchio Problem Daniel Spiewak - What is Hindley-Milner? (and why is it…
yehnan
  • 5,392
  • 6
  • 32
  • 38
38
votes
6 answers

What makes Haskell's type system more "powerful" than other languages' type systems?

Reading Disadvantages of Scala type system versus Haskell?, I have to ask: what is it, specifically, that makes Haskell's type system more powerful than other languages' type systems (C, C++, Java). Apparently, even Scala can't perform some of the…
Curry
  • 381
  • 1
  • 3
  • 3
30
votes
2 answers

Why does calling a method on a variable prevent Rust from inferring the type of the variable?

This code compiles: #[derive(Debug, Default)] struct Example; impl Example { fn some_method(&self) {} } fn reproduction() -> Example { let example = Default::default(); // example.some_method(); example } If the commented line is…
Shepmaster
  • 388,571
  • 95
  • 1,107
  • 1,366
28
votes
1 answer

Growth of Type Definition in SML Using Hindley Milner Type Inference

Someone once showed me a little 'trick' in SML where they wrote out about 3 or 4 functions in their REPL and the resulting type for the last value was extremely long (like many page scrolls long). Does anyone know what code generates such a long…
jkcorrea
  • 283
  • 3
  • 6
25
votes
2 answers

Inferred type appears to detect an infinite loop, but what's really happening?

In Andrew Koenig’s An anecdote about ML type inference, the author uses implementation of merge sort as a learning exercise for ML and is pleased to find an “incorrect” type inference. Much to my surprise, the compiler reported a type of 'a list ->…
Greg Bacon
  • 134,834
  • 32
  • 188
  • 245
23
votes
2 answers

What are the limits of type inference?

What are the limits of type inference? Which type systems have no general inference algorithm?
user141335
21
votes
1 answer

Damas-Hindley-Milner type inference algorithm implementation

I'm looking for information about the well-known Damas-Hindley-Milner algorithm to do type inference for functional languages, especially information about implementation. I already know how to do the Algorithm W, but I heard about recent new…
Vinz
  • 5,997
  • 1
  • 31
  • 52
20
votes
2 answers

Understanding Polytypes in Hindley-Milner Type Inference

I'm reading the Wikipedia article on Hindley–Milner Type Inference trying to make some sense out of it. So far this is what I've understood: Types are classified as either monotypes or polytypes. Monotypes are further classified as either type…
Aadit M Shah
  • 72,912
  • 30
  • 168
  • 299
18
votes
1 answer

What algorithm is used in Haskell (GHC) for deriving types of recursive expressions?

Consider the following examples: Non-recursive functions f x = x g y = f 'A' GHC infers f :: a -> a Mutually recursive functions f x = const x g g y = f 'A' Now GHC infers f :: Char -> Char, even though the type could be a -> a just in the…
Petr
  • 62,528
  • 13
  • 153
  • 317
14
votes
3 answers

Type inference implemented in C++

Is there an implementation in C++, of Damas-Hindley-Milner style type inference, preferably using modern C++ techniques?
keveman
  • 8,427
  • 1
  • 38
  • 46
14
votes
3 answers

Programmatic type annotations in Haskell

When metaprogramming, it may be useful (or necessary) to pass along to Haskell's type system information about types that's known to your program but not inferable in Hindley-Milner. Is there a library (or language extension, etc) that provides…
pash
  • 1,657
  • 1
  • 14
  • 29
13
votes
2 answers

Hindley-Milner algorithm in Java

I'm working on a simple dataflow based system (imagine it like a LabView editor/runtime) written in Java. The user can wire blocks together in an editor and I need type inference to ensure the dataflow graph is correct, however, most type inference…
akarnokd
  • 69,132
  • 14
  • 157
  • 192
12
votes
2 answers

Describe the Damas-Milner type inference in a way that a CS101 student can understand

Hindley-Milner is a type system that is the basis of the type systems of many well known functional programming languages. Damas-Milner is an algorithm that infers (deduces?) types in a Hindley-Milner type system. Wikipedia gives a description of…
user128807
  • 10,447
  • 17
  • 53
  • 72
11
votes
1 answer

Correct form of letrec in Hindley-Milner type system?

I'm having trouble understanding the letrec definition for HM system that is given on Wikipedia, here: https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Recursive_definitions For me, the rule translates roughly to the following…
exa
  • 859
  • 7
  • 27
1
2 3 4 5 6