Question about the type inference about sixten HOT 3 CLOSED

Hey!

Good question. I initially based the type inference on "Complete and Easy ..." (but with metavar handling based on http://okmij.org/ftp/ML/generalization.html). If I remember correctly (this was a couple of years ago) I couldn't come up with a way to adapt it to the setting where you have implicit arguments that can optionally be given explicitly, and found that easier with the "Practical ..." system. That was probably my fault though, and not the system's.

One advantage of "Complete and Easy ..." is that it gives details for how you can represent e.g. unification variables (which are in their "context"), so there are fewer details that have to be made up or extrapolated by you as the implementer. The exposition is also unusually clear, so in that sense it's easy to implement.

However, any time you try to base a "real-world" system on short research papers there's always going to be a lot of extrapolation (how to do mutually recursive top-level definitions, ADTs, or pattern matching?). I also don't think that the amount of code or its complexity will differ greatly whichever system you choose.

It's possible that I'll revisit this choice at some point, especially since there are a few planned extensions to Sixten's type system.

from sixten.

Ah okay, thanks for the detailed answer! Another question: how do you feel about impredicative instantiation? Neither "Complete..." or "Practical..." support this. Do you think you will need this feature or did you already decide it's not a necessity?

from sixten.

No problem!

It feels less clear cut when all you have is implicit arguments, but Sixten does not currently support it at least. I haven't really missed it in Haskell (well, maybe I would if it didn't have the hack for ($)?), so I'm hoping I won't miss it in Sixten either. :)

from sixten.