Skip to content

Latest commit

 

History

History
223 lines (162 loc) · 11.1 KB

type_inference.md

File metadata and controls

223 lines (162 loc) · 11.1 KB

Type inference

A Hindley–Milner (HM) type system is a classical type system for the lambda calculus with parametric polymorphism. Several Algorithms are described for infering HM types. Algorithm W, M

Various extensions exist, when considering extensions do they leave inference complete without annotations.

Extending algorithm with Constraints Wand https://www.cs.uwyo.edu/~jlc/papers/CIE_2008.pdf Wand and polymorphism https://www.win.tue.nl/~hzantema/semssm.pdf

Really nice W vs J write up https://www.ccs.neu.edu/home/amal/course/7480-s12/inference-notes.pdf

J impl https://github.com/quasarbright/AlgorithmJ/blob/master/src/Static/Context.hs J fast imple with levels https://github.com/jfecher/algorithm-j/blob/master/j.ml Best J explaination https://www.cl.cam.ac.uk/teaching/1415/L28/type-inference.pdf

Worth a read = https://okmij.org/ftp/ML/generalization.html#history

hm in go https://github.com/chewxy/hm Lazy copy all version of env

Type vs Kind

Values have types, types have Kinds Int, Maybe(Int), Fn(Int) -> Int all have kind * (Concrete types) Maybe has kind * -> * Type constructor

worth further investigation

  • MLsub for recursion
  • implement a iso vs equi recursion
  • ATSUSHI for rows
  • links-lang equirecursive types

Error messages

Error given is dependent on infer order. One thing is to move to constrains that might be reorderable. generalise and instantiate make this hard

Rows

Row types describe Extensible Record and Variant types. They do not define Enums or nominal type Seems like implicit Free Row types are kept around, how does this effect caching?

Row extension can be solved by ALWAY being modification, Don't know how this works for unions If we have unions for effects do we get the same need for tracking nope values. though a union won't crash if meaningless values are matched on which works for now. Is tracking unused branches the same complexity as keeping a list of not in row labels.

An ML-style Record Calculus with Extensible Records

We present an alternative construction based on the polymorphic record calculus developed by Ohori. Ohori based his polymorphic record calculus on the idea of kind restrictions. This allowed him to express polymorphic operations on records such as field selection and modification

Ohori does not allow extension because no representation of rows without a field

{foo = 5, ..b}
b.foo

Gaster and Jones [7] presented an elegant type system for records and variants based on the theory of qualified types [10, 11]. Special lacks predicates are used to prevent records from containing duplicate labels

In particular, as imposed by MLF, type annotations are only neces- sary when function arguments of an unknown type are used poly- morphically. !!!!

Read MLF or are there other ways allowing may instantiations I(a) = Int -> Int I(a) = String -> Int a = A -> Int I(a) = String -> String a = A -> B My language doesn't allow generic usage of a fn passed in.

Useful way of getting a never type out -> Never type, needed with Effects Return(Int) | Exp(String) how is generic function within a record handled in this paper

does always update allow us to drop free row variable?

Author Daan. Part of IFIP working group 2.16 on programming language design https://languagedesign.org/

Total fn type inference Dhall alpha reduction

Is recursive totality checking same or different to Dhall style inference.

  • fn polymorphism not let

  • row with only update

  • update access equi/iso ->

  • MLF needs annotation for generic parameters

  • MLSub vs record stuff

  • The scoped approach will work for dropping recursive check in fn, BUT we need to understand equi or not.

Koka structs? The koka paper talks about automatically opening records

Advanced

Recursion

hash consing is a technique used to share values that are structurally equal

hash("[5,Rec(0)]")
0.[Int, 0.[Int,0]]

overwrite(l = 4, r)

0.[[Some(0) | None]  4]
Some([[0 | None] 4])

Which paper always has a rec thing

Paper on first class cases talks about recursive types

Recursive data types

Recursion is fairly easily handled using a let rec construction and a fixpoint for type inference. However for trivial inference this only works for types that are not recursive or that are nominal. This doesn't work for structural typing.

Effect types

CPS

More of a compilation concern

Are continuations just first class control flow, do we need to call them effects as that is not really the case for for comprehensions Can we always CPS style with backpassing and perform is just bumping to the higher level If I want to handle a promise I need a different API http.get vs task.async(http.get)

Incremental

Flow analysis

A typesystem equivlent to flow analysis