Re: [Haskell-cafe] Explicitly calling syntactic equality on datatypes

On 18/09/2019 15.34, Juan Casanova wrote:

Quoting MarLinn 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.