The Calculated Typer

zacgarby

Hi! Author here. Very nice surprise to see this on the front page of HN this morning :) Happy to answer any questions if anybody has any!

efnx

From the abstract it sounds a bit like https://brianmckenna.org/blog/type_annotation_cofree, which is a great read.

knbknb

Q: There is not a single occurrence of the word "infer" (and related terms such as "inference") in the whole paper. Did you carefully try to avoid it or did this happen accidentally? Or is it the point of your paper?

(I encounter Type Checking only in my IDE when red squiggly lines appear under syntax errors etc. So consider this a layman Q)

mrkeen

The more complicated a type system is, the harder it is to make inference work.

Global type inference typically works well in Haskell without any hand-holding, but when you pack more features into the type system (e.g. in Idris), the programmer needs to explicitly write out more type signatures.

This type system looks "next-level complicated", so inference is probably way out of the question, e.g. if you saw the expression 2 + 3, maybe the types are:

  2 :: Head<Filter<IsPositive,[-1,-3,2,4]>>
  3 :: Head<Drop<4,Fibonnaci>>

If you were type-checking, you could start on the RHS, end up with the LHS, and then confirm that these two sub-expressions can be added. But with inference you're trying to figure out the most appropriate RHS from the LHS.