[Haskell-cafe] Explicitly calling syntactic equality on datatypes

[MarLinn]

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.