How to use Data Kinds + Phantom types to encode units in Haskell?

Question

The code below does not work because it does compile. It should not (intuitively).

1) Why does this code compile ?

2) How can I "fix" this program so that "bad" programs like isKm $ getMeter 1 is rejected during compile time ?

{-# LANGUAGE GADTs,StandaloneDeriving,DataKinds,ConstraintKinds,KindSignatures #-}

main=putStrLn "hw"

type Length (unit::LengthUnit)= Double
data LengthUnit= Km | Meter

divideByTwo ::Length lu->Length lu
divideByTwo l =l/2

getKm ::Double->Length Km
getKm d = d

getMeter ::Double->Length Meter
getMeter d =d

isKm :: Length Km ->Bool
isKm _ = True

this_should_not_compile_but_it_does=isKm $ divideByTwo $ getMeter 1

this_is_even_stranger_that_it_does_compile = isKm $ getMeter 1

Answer 1

The type keyword only creates an alias. For example type Foo = Bar just means that the compiler knows that you mean Bar whenever you say Foo. In this case this means that Length Km is equivalent to Double. The same is true for Length Meter. The compiler treats them both as Double and thus there is no difference between them.

The Data keyword however creates a new type rather than pointing to another one. by replacing type Length (unit::LengthUnit)= Double with data Length (unit::LengthUnit)= Len Double we create a new type which holds the Double within itself (constructed with Len).

The following code fails as desired:

{-# LANGUAGE GADTs,StandaloneDeriving,DataKinds,ConstraintKinds,KindSignatures #-}

main=putStrLn "hw"

data Length (unit::LengthUnit)= LenD Double
--type Length (unit::LengthUnit)= Double
data LengthUnit= Km | Meter

divideByTwo ::Length lu->Length lu
divideByTwo (LenD l) =LenD (l/2)

getKm ::Double->Length Km
getKm d =LenD d

getMeter ::Double->Length Meter
getMeter d =LenD d

isKm :: Length Km ->Bool
isKm _ = True

this_should_not_compile_but_it_does=isKm $ divideByTwo $ getMeter 1

this_is_even_stranger_that_it_does_compile = isKm $ getMeter 1

The following error was given from ghc code.hs:

[1 of 1] Compiling Main             ( code.hs, code.o )

code.hs:20:44:
    Couldn't match type 'Meter with 'Km
    Expected type: Length 'Km
      Actual type: Length 'Meter
    In the second argument of `($)', namely `divideByTwo $ getMeter 1'
    In the expression: isKm $ divideByTwo $ getMeter 1
    In an equation for `this_should_not_compile_but_it_does':
        this_should_not_compile_but_it_does
          = isKm $ divideByTwo $ getMeter 1

code.hs:22:53:
    Couldn't match type 'Meter with 'Km
    Expected type: Length 'Km
      Actual type: Length 'Meter
    In the return type of a call of `getMeter'
    In the second argument of `($)', namely `getMeter 1'
    In the expression: isKm $ getMeter 1

The error points out that we are getting Km and Meter mixed up.

Answer 2

It compiles because type doesn't introduce a new distinct type:

A type synonym declaration introduces a new type that is equivalent to an old type. [...]

Type synonyms are a convenient, but strictly syntactic, mechanism to make type signatures more readable. A synonym and its definition are completely interchangeable, [...]

Completely, without restrictions, at any level, including type signatures. You can see this with an even shorter example:

type Clown a b = Double

proof :: Clown a b -> Clown b a
proof = id

Since Clown a b and Clown b a are both Double—regardless of the actual a and b—both can be exchanged for Double, and proof's type is Double -> Double.

While your constraint limits the possible types for a in Length a, it doesn't actually change the se­man­tics of the resulting type. Instead, use a newtype:

data LengthUnit = Km | Meter
newtype Length (unit::LengthUnit) = MkLength {getLength :: Double}

onLength  :: (Double -> Double) -> Length a -> Length a
onLength f = MkLength . f . getLength

divideByTwo ::Length l -> Length l
divideByTwo = onLength (/ 2)

getKm ::Double -> Length Km
getKm = MkLength

-- other code omitted

Now you will get the desired compile term errors, because Length Km and Length Meter are distinct types:

test.hs:25:44:
    Couldn't match type 'Meter with 'Km
    Expected type: Length 'Km
      Actual type: Length 'Meter
    In the second argument of `($)', namely `divideByTwo $ getMeter 1'
    In the expression: isKm $ divideByTwo $ getMeter 1
    In an equation for `this_should_not_compile_but_it_does':
        this_should_not_compile_but_it_does
          = isKm $ divideByTwo $ getMeter 1

test.hs:27:53:
    Couldn't match type 'Meter with 'Km
    Expected type: Length 'Km
      Actual type: Length 'Meter
    In the second argument of `($)', namely `getMeter 1'
    In the expression: isKm $ getMeter 1