3

以下のコードはコンパイルされるため機能しません。そうすべきではありません（直感的に）。

1) このコードがコンパイルされるのはなぜですか?

isKm $ getMeter 12)コンパイル時に「悪い」プログラムが拒否されるように、このプログラムを「修正」するにはどうすればよいですか?

{-# 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— 実際のaandに関係なく — どちらbも と交換できるので、Doubleのproof型はDouble -> Doubleです。

制約によって in の可能な型が制限されますaが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が意味することを知っていることを意味します. この場合、これはと同等であることを意味します。についても同様です。コンパイラはそれらを両方として扱うため、両者に違いはありません。BarFooLength KmDoubleLength MeterDouble

ただし、Dataキーワードは、別のタイプを指すのではなく、新しいタイプを作成します。で置き換えることにより、それ自体の中に を保持する新しい型を作成しtype Length (unit::LengthUnit)= Doubleます( で構築されます)。data Length (unit::LengthUnit)= Len DoubleDoubleLen

次のコードは、必要に応じて失敗します。

{-# 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 に答える