In my previous post I discussed a solver plugin for
KnownNat constraints, and with regards to user-defined type-level operations, I said:
i.e. it cannot solve constraints involving subtraction (
-) or user-specified type-level operations on type-level naturals […] For user-defined type-level natural operations we are currently out of luck: unlike for the standard operations in
GHC.TypeLits, we cannot encode the corresponding dictionary functions beforehand.
well… it turns our we do not have to know these corresponding dictionary functions beforehand.
So, I'm hereby announcing version 0.2 of the ghc-typelits-knownnat plugin, which can now also solve
KnownNat constraints over types consisting of:
So what is the "trick" for handling user-defined operations?
Well, in my previous post, we defined a class, and corresponding instance for every type-level operation.
For example, for addition (
GHC.TypeLits.+), we defined:
And for multiplication (
GHC.TypeLits.*), we defined:
However, what we would want, is a single type class for functions of a certain arity, and subsequently define multiple instances for this single class. We can then export these type-classes, and developers can add an instance for their own type-level operations, and the solver plugin can then just lookup these instances.
Using some singletons trickery we can define such a type class as:
As it says in the comments, the first argument of this class is a type-level Symbol corresponding to the fully qualified name of the type-level operation.
We need to do this, because, unlike normal type constructors (.i.e.
Maybe), type families cannot be partially applied.
This means we cannot write a class and corresponding instance of the form:
So, instead, for the first argument of the
KnownNat2, we use a
Symbol that corresponds to the name of the type-level operation.
The solver plugin can then use the name of type-level operation to find the corresponding
Now, again due to the restriction on the partial application of type families, the associated type family
KnownNatF2 cannot be of kind:
Instead, we must use a defunctionalised form of our type-level operations, which are provided by the singletons package:
Where the difference is that we use
~> (tilde-right_angle) instead of
We can now define our addition and multiplication instances as:
instance (KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeLits.+" a b where type KnownNatF2 "GHC.TypeLits.+" = (:+$) natSing2 = SNatKn (natVal (Proxy @a) + natVal (Proxy @b)) instance (KnownNat a, KnownNat b) => KnownNat2 "GHC.TypeLits.*" a b where type KnownNatF2 "GHC.TypeLits.*" = (:*$) natSing2 = SNatKn (natVal (Proxy @a) * natVal (Proxy @b))
And subtraction as:
which gets an extra constraint that
KnownNat (a - b) only holds when
b <= a.
So now that we have a type-class for constraint-level arithmetic, what steps should a developer take so that her type-level functions are supported by the ghc-typelits-knownnat solver? We will give a short example.
Enable some language extensions
Import the required modules
Define the type-level operation
One restriction is that such a type-level operation must have at least two equations. This restriction is due GHC treating single-equation type families as type synonyms, which are expanded at the Core level.
That is, had we written our
Max operation as a single-equation operation:
KnownNat (Max x y) constraint would show up as
KnownNat (If (x <=? y) y x) inside the solver plugin.
And, consequently, the solver wouldn't be able to look up the
KnownNat2 instance of
Use Template Haskell to generate the defunctionalised form of the type-level operation:
This will create the following definitions:
where we need
And finally specify the
where we use the
nameToSymbol (exported by
GHC.TypeLits.KnownNat) function to converts a Template Haskell
Name to a
The ghc-typelits-knownnat solver plugin is now at version 0.2; and it supports:
Which might make you wonder: if it basically supports all type-level operations on
Nat, why isn't this version 1.0?
Well, I probably should have called it 1.0, and perhaps I will call it that in a next bugfix release. However, there are still some aspects that would be nice to add/fix: