Inference - Dhall

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

TheMatten

What's the status of type inference? Last time I looked into Dhall I was driven off by having to annotate all the polymorphic functions explicitly - but maybe it's just me being used to it in Haskell :slight_smile:

Nicholas Scheel

I want to implement it as an editor tool, in dhall-purescript, but I haven't had time to put the research into it. (I would do it a non-standard way.)

Some people were suggesting adding bidirectional type inference, but there were concerns about the maintenance burden for implementations, and the related projects stalled.

Additionally, there are a number of choices being made as the language grows that complicate inference in many ways (overloading operators like .), which I think would make standard bidirectional inference more difficult.

Nicholas Scheel

Basically it would be a tool that performs a "fill in holes" functions, for holes that represent inferrable types. But it has to be a highly global search, due to all of the ambiguity. Basically I would propose a monoid that combines information from various usages, plus a couple other features (like refinement, tracing, error handling, backtracking).

As one example of ambiguity, $1.label : $2 can mean:

  • $1 : $3 is a record of type $3 containing a field named label, and $2 is the type of that field named label in that record
  • $1 is itself a union type, and it is either a bare union label, whence $2 = $1, or it is a constructor-type label with data of type $3, whence $2 = $3 -> $1.

All of this type of information needs to be combined in a sensible manner, and it won't be straightforward. Luckily that's the worst case, the rest is more straightforward :wink:

TheMatten

@Nicholas Scheel thanks - so at the end, explicit type arguments are sort of a design decision?