参考資料:
- データ型の昇格(DataKinds拡張)|Haskellでの型レベルプログラミング
- 一般化された代数的データ型 (GADT)|Haskellでの型レベルプログラミング
- How can I use :~: to determine type equality in Haskell? - Stack Overflow
上記を参考に下記のコードを書いてみました。
エラーにならない:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind -- Type
import Data.Proxy
import Data.Type.Equality
foo :: Int ~ Int => () -- compiles fine
foo = ()
bar :: Int ~ Bool => () -- does technically compile
bar = ()
エラーになる:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind -- Type
import Data.Proxy
import Data.Type.Equality
foo :: Int ~ Int => () -- compiles fine
foo = ()
bar :: Int ~ Bool => () -- does technically compile
bar = ()
baz :: ()
baz = bar
エラー内容:
ghci> :load hoge.hs
[1 of 2] Compiling Main ( hoge.hs, interpreted )
hoge.hs:18:7: error: [GHC-18872]
• Couldn't match type ‘Int’ with ‘Bool’ arising from a use of ‘bar’
• In the expression: bar
In an equation for ‘baz’: baz = bar
|
18 | baz = bar
| ^^^
Failed, no modules loaded.
質問:
bar :: Int ~ Bool => () -- does technically compile
がエラーなく通ってしまうのは、下記にある :~: の定義 ように定義されているからでしょうか?- 私の理解は今回は aがInt, bがBoolなので、
a :~: a
がInt :~: Int
になってるのでOK(エラーなし)というような考えですが合っていますか?- だとするとEquality(型の等価性)がIntとBoolという違うものを同じとしていて、よくわかりません(というかbを使っていない。今回であればBoolを使っていない)。もしかしたら型の等価性をちゃんと理解できていないかもしれないです。
- そもそも
baz = bar
を増やしたコードだとエラーになる理屈もよくわかってませんが...
- 私の理解は今回は aがInt, bがBoolなので、
:~: の定義
type (:~:) :: k -> k -> Type data a :~: b where Refl :: a :~: a
質問まではいかないがわかっていないこと
- そもそもなんで急に
a :~: b
やa :~: a
のような中間演算子のような記法が出てきてるのか(Haskellで普通に許される記法?)
補足
型の等価性については シンボル、構文木、型 | Reflection | Scala Documentation に =:= メソッド
というのがあり、これが :~:
と同じなのか試したいのですが、HakellもScalaも不慣れなので同じのがありそうとしか認識できていません。
追記:
https://ja.stackoverflow.com/a/99261/9008 の回答を受けて完全に読み違えていたので、そもそも試すコードが間違えていました。
本当に試したかった部分を自分なりに試してみました。
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind -- Type
import Data.Proxy
type (:~:) :: k -> l -> Type
data a :~: b where
Hoge :: x :~: x
foo2 :: Int :~: Int -> ()
foo2 proof
= case proof of
Hoge -> ()
1文字変数のところで別の名前をつけれるところは変えてみました。
これで Int :~: Int
はエラーなし。 Bool :~: Int
はエラーになりました。
x :~: x
のところは x :~: y
にするとうまく判定できていませんでした(Bool :~: Int
でもエラーなし)。
追記質問:
TypeOperatorsのこの記法は、Algebraic Data Typesと同じ(Algebraic Data Typesの延長にある)もので、データを保持するような型を定義していると考えよいのでしょうか?
試しに下記のようにしてみると Bool :~: Int
でもエラーにならないので、パターンマッチング部分とも関連しながら、等価性を判定しているようですが、データを保持するというメンタルモデルとパターンマッチングと型の等価性がうまく脳内で結びつきません。
foo2 proof
= ()