[Haskell-cafe] Explicitly calling syntactic equality on datatypes
MarLinn
monkleyon at gmail.com
Wed Sep 18 17:07:52 UTC 2019
On 18/09/2019 15.34, Juan Casanova wrote:
> Quoting MarLinn <monkleyon at gmail.com> on Wed, 18 Sep 2019 14:53:32 +0200:
>
>> What about phantom types?
>>
>> {-# LANGUAGE KindSignatures, DataKinds #-}
>> data IsNormalized = Normalized | NotNormalized
>> data Sum (n :: IsNormalized) = Value Int | Sum (Sum n) (Sum n)
>>
>> normalizeSum :: Sum NotNormalized -> Sum Normalized -- or even
>> create a class with two inhabitants for this
>> instance Eq (Sum NotNormalized) where (==) = (==) `on` normalizeSum
>> instance Eq (Sum Normalized) where … -- real implementation
>
>
> That looks quite good tbh. I did not know you could do that. Care to
> explain, are "Normalized" and "NotNormalized" types, data
> constructors, type families? A combination of them?
I'm not an expert, so I apologize if I get some of the details wrong.
This is all a trick with kinds. Kinds are to types as types are to values.
The key is in the two extensions. DataKinds allows you to use data as
kinds. So it's possible to use IsNormalized as a kind inhabited by the
two types Normalized and NotNormalized in the same ways as you can use
the kind * that is inhabited by all "normal" types. Note that types of
kind * are also in turn inhabited by values; types of kind IsNormalized
are not, so you can only use it and it's types in signatures for now.
KindSignatures then allows you to use the signature in the definition of
Sum which tells GHC that the first parameter of Sum has this new kind,
so only its inhabitants can be used in this place.
You can check this by asking GHCI ":kind Sum". It will tell you that
"Sum :: IsNormalized -> *", so Sum has a kind that takes a type of kind
IsNormalized and returns a kind of the usual type *.
Hope that helps.
More information about the Haskell-Cafe
mailing list