- Hindley-Milner Type Inference & Type Systems
- This content explores the concepts of Hindley-Milner type inference, type systems, parameterized types, explicit polymorphism, and implicit polymorphism in programming languages. It discusses how programmers declare types for variables and the use of generics in languages like Java and C#. The examples illustrate type declarations, polymorphism, and type parameter handling in different contexts.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Hindley-Milner Type Inference CSE 340 Principles of Programming Languages Fall 2015 Adam Doup Arizona State University http://adamdoupe.com
Type Systems In what we have seen so far, the programmer must declare the types of the variables array [0..5] of int a; int i; a[i] = 1; 2 Adam Doup , Principles of Programming Languages
Type Systems In what we have seen so far, the programmer must declare the types of the variables array [0..5] of int a; string i; a[i] = 1; 3 Adam Doup , Principles of Programming Languages
Type Systems In what we have seen so far, the programmer must declare the types of the variables array [0..5] of int a; int i; a[i] = "testing"; 4 Adam Doup , Principles of Programming Languages
Parameterized Types Some languages allow the programmer to declare parameterized types Instead of being specific to a given type, the specific type is given as a parameter Generics in Java and C#, templates in C++ 5 Adam Doup , Principles of Programming Languages
import java.util.Random; public class Chooser{ static Random rand = new Random(); public static <T> T choose(T first, T second) { return ((rand.nextInt() % 2) == 0)? first: second; } } class ParameterizedTypes{ public static void main(String [] args) { int x = 100; int y = 999; System.out.println(Chooser.choose(x, y)); String a = "foo"; String b = "bar"; System.out.println(Chooser.choose(a, b)); } } 6 Adam Doup , Principles of Programming Languages
Explicit Polymorphism Note that in the previous example, the programmer must declare the parameterized types explicitly Slightly different polymorphism than what is used in the object orientation context The compiler/interpreter will allow a function to be called with different types (while still checking for type compatibility) 7 Adam Doup , Principles of Programming Languages
Implicit Polymorphism The programmer does not need to specify the type parameters explicitly Dynamic languages have this property too However, the type checker will, statically, attempt to assign the most general type to every construct in the program 8 Adam Doup , Principles of Programming Languages
Implicit Polymorphism fun foo(x) = x What is the type of foo? Function of T returns T (T) -> T fun foo(x) = x; fun bar(y) = foo(y); What is the type of bar and foo? foo: Function of T returns T (T) -> T bar: Function of T returns T (T) -> T 9 Adam Doup , Principles of Programming Languages
Implicit Polymorphism fun max(x, y) = if x < y then y else x What is the type of max? Function of (int, int) returns int (int,int) -> int 10 Adam Doup , Principles of Programming Languages
Implicit Polymorphism fun max(cmp, x, y) = if cmp(x,y) then y else x What is the type of max? Function of (Function of (T, T) returns bool, T, T) returns T ((T, T) -> bool, T, T) -> T max(<, 10, 200) max(strcmp, "foo", "bar") 11 Adam Doup , Principles of Programming Languages
Implicit Polymorphism fun foo(a, b, c) = c(a[b]) What is the type of foo? Function of (Array of T, int, Function of (T) returns U) returns U (Array of T, int, (T -> U)) -> U 12 Adam Doup , Principles of Programming Languages
Implicit Polymorphism fun foo(a, b, c) = a = 10; a(b[c]); What is the type of foo? Type error! 13 Adam Doup , Principles of Programming Languages
Hindley-Milner Type Checking Hindley-Milner type checking is a general type inference approach It infers the types of constructs that are not explicitly declared It leverages the constraints of the various constructs It applies these constraints together with type unification to find the most general type for each construct (or can find a type error if there is one) Full Hindley-Milner type checking is used in OCaml, F#, and Haskell 14 Adam Doup , Principles of Programming Languages
Type Constraints To apply Hindley-Milner, we must first define the type constraints Constant integers , -1, 0, 1, 2, ... Type = int Constant real numbers ..., 0.1, 2.2, ... other floating point numbers Type = real Constant booleans true or false Type = boolean Constant strings "foo", "bar", ... Type = string 15 Adam Doup , Principles of Programming Languages
Operators Relational Operators a op b (T1) op (T2) a (T3) b op is <, <=, >, >=, !=, == T1 = boolean T2 = T3 = numeric type 16 Adam Doup , Principles of Programming Languages
Operators Arithmetic Operators a op b (T1) op (T2) a (T3) b op is +, -, *, / T1 = T2 = T3 = numeric type 17 Adam Doup , Principles of Programming Languages
Operators Array Access Operator a[b] (T1) [] (T2) a (T3) b T2 = array of T1 T3 = int 18 Adam Doup , Principles of Programming Languages
Function Application foo(x1, x2, , xk) (R) apply (F) foo (T1) x1 (T2) x2 (Tk) xk F = (T1, T2, , Tk) -> R 19 Adam Doup , Principles of Programming Languages
Function Definition fun foo(x1, x2, , xk) = expr fun F T1, T2, , Tk foo (x1, x2, , xk) (E) expr F = (T1, T2, , Tk) -> E 20 Adam Doup , Principles of Programming Languages
If Expression if (cond) then expr1 else expr2 (T4) if (T1) cond (T2) expr1 (T3) expr2 T1 = boolean T2 = T3 = T4 21 Adam Doup , Principles of Programming Languages
Type Unification Type unification is the process by which the constraints are propagated Basic idea is simple Start from the top of the tree Every time you see a construct with unconstrained types, create a new type If a construct is found to have type T1 and also to have type T2, then T1 and T2 must be the same type 22 Adam Doup , Principles of Programming Languages
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (3) c (4) [] a b c (5) a (6) b (1) (2) (3) (4) (5) 23 Adam Doup , Principles of Programming Languages (6)
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (3) c (4) [] a T1 T2 T3 b c (5) a (6) b (1) (2) (3) (4) (5) 24 Adam Doup , Principles of Programming Languages (6)
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (T1,T2,T3) -> T4 T1 T2 T3 (3) c (4) [] a b c (5) a (6) b (1) (2) (3) (4) (5) 25 Adam Doup , Principles of Programming Languages (6)
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (T1,T2,T3) -> T4 T1 T2 T3 (3) c (4) [] a b c (5) a (6) b (1) (2) T4 (3) (4) (5) 26 Adam Doup , Principles of Programming Languages (6)
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (T1,T2,T3) -> T4 T1 T2 T3 (3) c (4) [] a b c (5) a (6) b (1) (2) T4 (3) (4) T5 (5) 27 Adam Doup , Principles of Programming Languages (6)
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (T1,T2,T3) -> T4 T1 T2 T3 (3) c (4) [] a b c (5) a (6) b (1) (2) T4 T5 -> T4 T5 (3) (4) (5) 28 Adam Doup , Principles of Programming Languages (6)
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (T1,T2,T3) -> T4 T1 T2 T5 -> T4 (3) c (4) [] a b c (5) a (6) b (1) (2) T4 T5 -> T4 T5 (3) (4) (5) 29 Adam Doup , Principles of Programming Languages (6)
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (T1,T2,(T5->T4)) -> T4 T1 T2 T5 -> T4 (3) c (4) [] a b c (5) a (6) b (1) (2) T4 T5 -> T4 T5 (3) (4) (5) 30 Adam Doup , Principles of Programming Languages (6)
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (T1,T2,(T5->T4)) -> T4 T1 T2 T5 -> T4 (3) c (4) [] a b c (5) a (6) b (1) (2) T4 T5 -> T4 T5 Array of T5 (3) (4) (5) 31 Adam Doup , Principles of Programming Languages (6)
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (T1,T2,(T5->T4)) -> T4 T1 T2 T5 -> T4 (3) c (4) [] a b c (5) a (6) b (1) (2) T4 T5 -> T4 T5 Array of T5 (3) (4) (5) 32 Adam Doup , Principles of Programming Languages (6) int
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (Array of T5 ,T2,(T5- >T4)) -> T4 Array of T5 T2 T5 -> T4 (3) c (4) [] a b (5) a (6) b c (1) (2) T4 T5 -> T4 T5 (3) (4) Adam Doup , Principles of Programming Languages (5) Array of T5 (6) int 33
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (Array of T5, T2,(T5->T4)) -> T4 Array of T5 int (3) c (4) [] a b (5) a (6) b c T5 -> T4 (1) (2) T4 T5 -> T4 T5 (3) (4) Adam Doup , Principles of Programming Languages (5) Array of T5 (6) int 34
fun foo(a, b, c) = c(a[b]) (1) def (2) apply foo (a, b, c) foo (Array of T5, int,(T5->T4)) -> T4 Array of T5 int (3) c (4) [] a b (5) a (6) b c T5 -> T4 (1) (2) T4 T5 -> T4 T5 (3) (4) Adam Doup , Principles of Programming Languages (5) Array of T5 (6) int 35
