如何使用Data Kinds + Phantom类型对Haskell中的单元进行编码？

下面的代码不起作用,因为它不编译.它不应该(直观地).

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

Zeta.. 9

它编译因为type没有引入新的不同类型:

类型同义词声明引入了一种等同于旧类型的新类型.[...]

类型同义词是一种方便但严格的语法机制,可使类型签名更具可读性.同义词及其定义完全可以互换, [...]

完全,无任何限制,在任何级别,包括类型签名.你可以用一个更短的例子看到这个:

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.

虽然约束限制了ain 的可能类型Length 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

HEGX64.. 6

该type关键字只创建一个别名.例如type Foo = Bar只是意味着编译器知道你的意思是Bar,只要你说的Foo.在这种情况下,这意味着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混淆.

它编译因为type没有引入新的不同类型:

类型同义词声明引入了一种等同于旧类型的新类型.[...]

类型同义词是一种方便但严格的语法机制,可使类型签名更具可读性.同义词及其定义完全可以互换, [...]

完全,无任何限制,在任何级别,包括类型签名.你可以用一个更短的例子看到这个:

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.

虽然约束限制了ain 的可能类型Length 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

该type关键字只创建一个别名.例如type Foo = Bar只是意味着编译器知道你的意思是Bar,只要你说的Foo.在这种情况下,这意味着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混淆.