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

Question

下面的代码 不起作用 因为它可以编译。它不应该（凭直觉）。

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

2) 我如何 "fix" 这个程序，以便 "bad" 像 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

Answer 2

type 关键字仅创建一个别名。例如 type Foo = Bar 只是意味着编译器知道你在说 Foo 时的意思是 Bar。在这种情况下，这意味着 Length Km 等同于 Double。 Length Meter也是如此。编译器将它们都视为 Double，因此它们之间没有区别。

Data 关键字创建了一个新类型而不是指向另一个类型。通过将 type Length (unit::LengthUnit)= Double 替换为 data Length (unit::LengthUnit)= Len Double，我们创建了一个新类型，它在自身内部包含 Double（由 Len 构建）。

以下代码按预期失败：

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

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

错误指出我们混淆了 Km 和 Meter。

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

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

haskell

phantom-types

data-kinds