Tripping up type inference
source link: https://www.tuicool.com/articles/N7VRnmR
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
One of the main selling points of Haskell is that despite (or because) of its strong static type system, it frees us from the burden of having to spell out tedious type signatures everywhere.
Type inference is a blessing, but sometimes it can also be a curse. Inference too good can hinder the readability of code, because the compiler knows what the type of an identifier is even when we don’t. It’s not just readability though: correctness can be imperilled too.
As an example, consider the Tagged
type, which allows
us to attach type information to some other type.
newtype Tagged (s :: k) a = MkTagged a
Then we might want to define a Person
type consisting of a first
name and a last name, both of type String
, tagged by (type-level)
symbols accordingly:
data Person = MkPerson (Tagged "firstName" String) (Tagged "lastName" String)
We can then construct values of this type:
joseph :: Person joseph = MkPerson (MkTagged "Joseph") (MkTagged "Knecht")
And here is the problem. Since both fields are constructed just with
the MkTagged
constructor, nothing is stopping us from mixing up the
field names if we misremember the ordering:
joseph' :: Person joseph' = MkPerson (MkTagged "Knecht") (MkTagged "Joseph")
We would wish to get a type error, but GHC happily infers that MkTagged "Joseph"
indeed has type Tagged t String
for any t
,
thus it fits perfectly into the "lastName"
field.
We can fix this example by providing explicit type applications to
the MkTagged
constructor. Then, mixing up the order is
a type error.
joseph' :: Person joseph' = MkPerson (MkTagged @"lastName" "Knecht") (MkTagged @"firstName" "Joseph")
results in:
• Couldn't match type ‘"lastName"’ with ‘"firstName"’
This works, but these annotations are entirely optional, and if we forget about them, we’re in trouble once again.
To summarise, the problem is that GHC can infer the type of MkTagged "Joseph"
,
and due to the generality of the result, it can also unify
it with any arbitrary tag.
So the question is this: how do we stop GHC from inferring the type of
expressions like MkTagged "Joseph"
? In other words, how do we enforce
that the tag must be provided by explicit type annotation?
An ambiguous smart constructor
We’re going to write a smart constructor that can only be invoked by explicit type annotation of the tag type.
mkTagged :: forall t a. a -> Tagged (???) a mkTagged = MkTagged
What to put in the ???
hole? The idea is that we want t
in this
type to be ambiguous
, in other words, it should be impossible to
infer t
even if we know what Tagged (???) a
is. If it can’t be
inferred, then GHC will insist that we specify a type annotation at
the use site for what t
should be.
The obvious thing to plug into ???
would be t
itself, but that
doesn’t work of course, because from knowing Tagged t a
, t
can be
trivially inferred.
For example, when given a value of type Tagged "firstName" String
,
we can infer that t
must be "firstName"
.
As always (at least this seems to be a recurring theme here on my
blog), we reach for type families to solve this problem. In
particular, we define a rather funny-looking variant of the identity
type family, which I’m going to call Ambiguous
:
type family Ambiguous (a :: k) :: j where Ambiguous x = x
The first thing that might strike you is the kind signature: Ambiguous
takes an argument of kind k
, and returns something of
kind j
. It helps to think of these kind parameters as additional inputs
to the type family.
That is, Ambiguous "firstName"
will get stuck:
>>> :kind! Ambiguous "firstName" Ambiguous "firstName" :: j = Ambiguous "firstName"
because GHC doesn’t know at which j
we want to evaluate the type
family (and indeed, in principle this choice could change the
behaviour of the type family, since in GHC, type families are not
parametric).
In order to properly reduce the family, we must provide the result kind as an input, like so:
>>> :kind! (Ambiguous "firstName" :: Symbol) (Ambiguous "firstName" :: Symbol) :: Symbol = "firstName"
Now let us plug this type family into the type of mkTagged
, and see what happens.
mkTagged :: forall t a. a -> Tagged (Ambiguous t) a mkTagged = MkTagged
Now, when GHC’s given Ambiguous t
, it can’t work out what t
is. Why? Suppose we know that Ambiguous t :: Symbol
, that is, we
expect it to reduce to a symbol. That still doesn’t tell us anything
about the kind of t
! According to the kind signature of Ambiguous
, the
kind of t
could be anything
. Indeed, the only way to disambiguate this
is to provide the kind of t
. As the signature of mkTagged
does
not have an explicit kind annotation on t
, the only way to provide
the kind of t
is to provide t
itself (since only visibly quantified
variables can be applied with visible type applications).
Now, the following code
joseph :: Person joseph = MkPerson (mkTagged "Joseph") (mkTagged "Knecht")
results in the error:
• Couldn't match type ‘Ambiguous t0’ with ‘"firstName"’
To fix it, we now must provide type applications:
joseph :: Person joseph = MkPerson (mkTagged @"firstName" "Joseph") (mkTagged @"lastName" "Knecht")
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK