First Class Polymorphism and Boolean Unification #6970
Superstar64
started this conversation in
Ideas
Replies: 1 comment 1 reply
-
@Superstar64 Thanks for the detailed write-up. It will probably take a bit for me to grok all the details. Meanwhile, do we have any good use cases? I guess one use case would be for higher-ranked effect polymorhism? Or perhaps higher-ranked nullability? But I cannot yet imagine how such program examples would look like. |
Beta Was this translation helpful? Give feedback.
1 reply
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
As requested from the Gitter, How to combine first class polymorphism and boolean unification:
Hindley Milner vs System-F
Hindley Milner is a type system where it is possible to do complete type inference without any type annotations, but it has limited expressability. Dually, System-F (first class polymorphism) is a much more expressive type system, but it's impossible to perform complete type inference without any type annotations.
There many systems that combine Hindley Milner and System-F. I would recommend the related work section of FreezeML and Quick Look for a good overview of the current state of the research.
Mixed Prefix Unification
A common necessity these systems have is mixed prefix unification (fair warning, this paper is somewhat dated and hard to read). Mixed prefix unification is a generalization of normal unification that allows you to have rigid type variables that don't unify with unification variable in a higher level. They need this to be able to unify higher rank types and first class polymorphism1. Let me go over some mixed prefix unification examples then generalize them to boolean unification. I should note that I'm going subset of mixed unification that rejects everything that needs higher order unification.
Example 1 (Normal Unification)
This is just normal unification that you would expect to see in normal Hindley Milner. Here
X = b
andY = a
.Example 2 (Swaped Qualifiers)
This is just like the previous example except the existential and universal qualifiers swapped. This example would error out (again without higher order unification) because
X
is trying to unify withb
, which is a variable is a higher level. These sort of equations are the cause of skolemization errors that you commonly see in Haskell when using RankNTypes.Example 3 (Forall)
This example shows why mixed prefix unification is needed in the first place. It's used when you want to unify forall types. You just simply pick fresh variables and substitute them into the qualify then you augment them as a fresh skolem variable.
Example 4 (No Higher Order Unification)
This last example shows something that could be solved with higher order unification but that is typically rejected for simplicity.
Constant Elimination
As I already mentioned, for mixed prefix unification to work, you need to make sure you don't allow a variable to unify with a constant at a higher level. This is normally something you just deal with when implementing it but can actually convert these problem into normal unification(thanks to @mb64 for this idea). What you do is pick two types that you know are different and you duplicate your problem set substituting one type to one universal qualifier respectively.
Lets say here
Int
andChar
are chosen as two types that we know are different. Here's how you would do this with the second example:As expected this would error out. Trying to unify a variable with a higher constant is translated to the variable being equal to two types at once.
Now for the translation of the third example:
Here as expected this doesn't error out. The variable is never unified with a higher level constant, so gets translated into redundant equations.
Mixed Prefix Boolean Unification
Luckily for boolean unification there are always two booleans that we know aren't equal (
true
andfalse
). So know let me take all this together and use this to solve a unification problem with a higher rank type that involves boolean unification:In summary, if Flix ever wants first class polymorphism. Your probably going to need an augmented form of mixed prefix unification that deletes constants for boolean equations via this duplication method I showed.
Footnotes
Higher rank types are a subset of System-F (first class polymophism), where the
forall
s are not wrapped by type constructors. IE(forall a. a) -> ...
but notList (forall a. a)
. ↩Beta Was this translation helpful? Give feedback.
All reactions