3

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

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
4

2 回答 2

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
于 2016-01-02T12:49:10.097 回答
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。

于 2016-01-02T12:50:02.680 回答