haskell - 如何使用 Data Kinds + Phantom types 对 Haskell 中的单元进行编码？

Question

下面的代码不起作用，因为它可以编译。 (直觉上)不应该。

1) 为什么这段代码可以编译？

2) 我怎样才能“修复”这个程序，以便在编译时拒绝像 isKm $ getMeter 1 这样的“坏”程序？

{-# 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

它可以编译，因为 type 没有引入 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, [...]

完全、无限制、在任何级别，包括类型签名。您可以通过一个更短的示例来了解这一点:

type Clown a b = Double

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

因为 Clown a b 和 Clown b a 都是 Double - 无论实际的 a 和 b——两者都可以互换为Double，并且proof的类型是Double -> Double。

虽然您的约束限制了 Length a 中 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

现在您将得到所需的编译术语错误，因为 Length Km 和 Length Meter 是不同的类型:

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