1

参考資料:

上記を参考に下記のコードを書いてみました。

エラーにならない:

{-# 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 :~: aInt :~: Int になってるのでOK(エラーなし)というような考えですが合っていますか?
      • だとするとEquality(型の等価性)がIntとBoolという違うものを同じとしていて、よくわかりません(というかbを使っていない。今回であればBoolを使っていない)。もしかしたら型の等価性をちゃんと理解できていないかもしれないです。
      • そもそも baz = bar を増やしたコードだとエラーになる理屈もよくわかってませんが...

:~: の定義

type (:~:) :: k -> k -> Type
data a :~: b where
  Refl :: a :~: a

質問まではいかないがわかっていないこと

  • そもそもなんで急に a :~: ba :~: 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
  = ()

1 件の回答 1

1

bar :: Int ~ Bool => () -- does technically compile がエラーなく通ってしまうのは、下記にある :~: の定義 ように定義されているからでしょうか?

いいえ、違います。参考になさっている https://stackoverflow.com/a/71494201/5989200 にも書かれているように、~:~: は別物です。

今回出てきた ~Equality Constraints と呼ばれているものであり、型注釈に出てくる型変数に対して制約を加えるものです。リストをソートする関数の型を sort :: Ord a => [a] -> [a] と書くときの Ord a が制約を表しているのと同じで、今回の Int ~ Bool も制約になっています。

注意すべきこととして、この制約が検査されるのはこの関数が呼び出されている箇所についてです。関数定義の本体の部分ではこの制約は仮定として扱われます。関数を呼び出そうとして初めて、型検査の一環で制約の検査も行われます。というより、型変数が入りうるので呼び出す前に検査するようなものになりません。したがって bar :: Int ~ Bool => () を定義しただけだと Int ~ Bool なのかどうかまでは検査されず、baz = bar と呼び出そうとした際に検査されエラーになったという訳です。

対して、:~: は制約ではありません。型パラメーターをふたつ持つ型です。型であるという意味で、これは sort :: Ord a => [a] -> [a] の例だと [a] と同じ類のものです。なので https://stackoverflow.com/a/71494201/5989200 に載っている例のように、TypeOperators 拡張のもとで、

foo2 :: Int :~: Int -> ()
foo2 proof
  = case proof of
      Refl -> ()

というように使うことになります。定義も以下のようになっており、a :~: a で「:~: の両辺に同じ型が与えられる」場合のみ型検査が通るようになっていることが読み取れます。

type (:~:) :: k -> k -> Type
data a :~: b where
  Refl :: a :~: a

補足::~: が中置記法で使えるのは、Haskell では特定の記号で始まる関数はデフォルトで中置できるような構文規則になっているためです。

9
  • 「~ と :~: は別物」だったんですね。完全に読み違えていました。 foo2 proof の使用イメージがつかないのですが、実際にfoo2を使う例をご提示いただけないでしょうか。 Commented 5月3日 11:04
  • 関数呼び出しをしたいという意味であれば、foo2 Refl です。
    – nekketsuuu
    Commented 5月3日 12:03
  • 関数呼び出しという意味です。 なるほど。 foo2 1 :~: 1 とか foo2 Refl 1 1 とかfoo2 Int :~: int ではないんですね。 Commented 5月3日 12:06
  • オブジェクトレベルの構文と型レベルの構文とを区別してください。1Refl はオブジェクトレベルの値、Int:~: は型です。
    – nekketsuuu
    Commented 5月3日 12:12
  • オブジェクトレベルの構文と型レベルの構文の理解が曖昧なのもよくわからない原因の一つではあるかもしれないです。そもそも回答を受けて、試すコード自体が間違っていたので、質問を追記しました(別途質問を立てようかと悩みましたが) Commented 5月3日 23:44

この質問に回答するには、ログインする必要があります。

求めていた回答ではありませんか? のタグが付いた他の質問を参照する。