The Calculated Typer

efnx

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

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!

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)

zacgarby

Very good question! Funnily enough, it was indeed a conscious decision to avoid mentioning "inference", because then people might expect that we're doing polymorphism with type variables/or maybe that we're deriving a Hindley-Milner inference system.

We're not doing these things, so we figured it would be safer this way, but absolutely you could call what we're doing "type inference".

That being said, we've got some ideas for a follow-up paper to revisit this and derive something more worthy of being called "inference".

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.