23

型レベルの論理和を次のように定義しました。

{-# LANGUAGE DataKinds, TypeFamilies #-}

type family Or (a :: Bool) (b :: Bool) :: Bool
type instance Or False a = a
type instance Or True a = True

ここで、それが冪等であることを (Haskell で) 証明したいと思います。つまり、idempタイプで用語を構築したい

idemp :: a ~ b => proxy (Or a b) -> proxy a

これは、操作上は と同等idです。(もちろん、たとえば のように定義することもできますunsafeCoerceが、それはごまかしです。)

出来ますか？

4

2 に答える 2

15

あなたが求めていることは不可能ですが、代わりにかなり似たようなことができるかもしれません. 証明には型レベルのブール値のケース分析が必要なため不可能ですが、そのようなイベントを発生させるためのデータがありません。修正は、シングルトンを介してそのような情報を含めることです。

idempまず、タイプ forが少し難読化されていることに注意してください。制約a ~ bは、同じものを 2 回指定するだけです。次の型チェック:

idemq :: p (Or b b) -> p b
idemq = undefined
idemp :: a ~ b => p (Or a b) -> p a
idemp = idemq

( を含まない制約a ~ tがある場合、通常は を代用するのが良いでしょう。例外は宣言にあります:インスタンスの先頭にある an は何にでも一致するため、そのものが明らかに になっていなくても、インスタンスは起動します。しかし、私は余談。）tatainstanceat

idemqについて有用な情報がないため、定義できないと主張しbます。利用可能な唯一のデータは inhabit p-of-something であり、何が何であるかはわかりませんp。

の場合によって推論する必要がありbます。一般的な再帰型ファミリでは、どちらTrueでもない型レベルのブール値を定義できることに注意してFalseください。スイッチをオンにするとUndecidableInstances、定義できます

type family Loop (b :: Bool) :: Bool
type instance Loop True = Loop False
type instance Loop False = Loop True

したがって、またはにLoop True還元することはできず、局所的にさらに悪いことに、それを示す方法はありません。TrueFalse

Or (Loop True) (Loop True) ~ Loop True     -- this ain't so

それから抜け出す方法はありません。b私たちのが何らかの形で値を計算する適切に動作するブール値の 1 つであるという実行時の証拠が必要です。だから歌おう

data Booly :: Bool -> * where
  Truey   :: Booly True
  Falsey  :: Booly False

が分かればBooly b、事例分析を行うことができ、何が何でbあるかがわかります。その後、各ケースはうまく処理されます。PolyKindsuses を抽象化するのではなく、 で定義された等価型を使用して事実をまとめる方法を次に示しますp b。

data (:=:) a b where
  Refl :: a :=: a

私たちの重要な事実は、今では明白に述べられ、証明されています。

orIdem :: Booly b -> Or b b :=: b
orIdem Truey   = Refl
orIdem Falsey  = Refl

そして、厳密なケース分析によってこの事実を展開できます。

idemp :: Booly b -> p (Or b b) -> p b
idemp b p = case orIdem b of Refl -> p

事例分析は厳密でなければなりません。証拠が馬鹿げた嘘ではなく、型を修正するために必要なRefl証拠だけを黙って詰め込んでいる善良な正直者であることを確認するためです。Or b b ~ b

これらすべてのシングルトン値を明示的にスリングしたくない場合は、kosmikus が示唆するように、それらを辞書に隠して、必要なときに抽出することができます。

Richard Eisenberg と Stephanie Weirich には、これらのファミリとクラスをミリングする Template Haskell ライブラリがあります。彼女もそれらを構築することができ、あなたは書くことができます

orIdem pi b :: Bool. Or b b :=: b
orIdem {True}   = Refl
orIdem {False}  = Refl

にpi b :: Bool.展開されforall b :: Bool. Booly b ->ます。

しかし、それはとてもつまらないものです。そのため、私のギャングは Haskell に real を追加することに取り組んでいます。これは、Haskell の型言語と用語言語の間の重要な共通部分でインスタンス化できるノンパラメトリック量指定子 ( and とはpi異なります) です。これには、引数がデフォルトで隠されている「暗黙の」バリアントもある可能性があります。2 つはそれぞれシングルトン ファミリとクラスの使用に対応しますが、追加のキットを取得するためにデータ型を 3 回定義する必要はありません。forall->pi

完全な型理論では、実行時にブール値の余分なコピーを渡す必要がないことに言及する価値があるかもしれません。b問題は、データが から にb転送される可能性があることを証明するためだけに使用されp (Or b b)、p b必ずしも転送されるデータを作成するためではないということです。実行時にバインダーの下で計算しないため、方程式の不正な証明を作成する方法はありません。したがって、証明コンポーネントを消去して、そのコピーbを配信することができます。Randy Pollack が言うように、強力に正規化する微積分で作業することの最も良い点は、物事を正規化する必要がないことです。

于 2013-03-03T11:13:46.593 に答える
7

John L がコメントで述べているように、現在、私の知る限り、追加の制約なしにこれを行う方法はありません。が用語レベルで閉じた種類であるという事実を利用することはできず、Boolの種類の型変数の場合分けを行う方法はありませBoolんidemp。

Bool典型的な解決策は、シングルトン型を使用して用語レベルで種類構造を反映することです。

data SBool :: Bool -> * where
  SFalse :: SBool False
  STrue  :: SBool True

任意の の場合、 (モジュロ、もちろん) のb :: Bool住民は 1 つだけです。SBool bundefined

を使用SBoolすると、定理は簡単に証明できます (なぜ余分な等式制約を追加したのかわかりません。削除します)。

idemp' :: SBool a -> proxy (Or a a) -> proxy a
idemp' SFalse x = x
idemp' STrue  x = x

SBool引数を明示的に渡す代わりに、表現を作成できるクラスを定義することにより、暗黙的に渡すことができます。

class CBool (b :: Bool) where
  sBool :: SBool b

instance CBool True  where sBool = STrue
instance CBool False where sBool = SFalse

それで：

idemp :: CBool a => proxy (Or a a) -> proxy a
idemp = idemp' sBool

CBool制約を取り除くことはできないと思いますが、どの にも自明に当てはまるa :: Boolので、あまり強い仮定ではありません。

于 2013-03-03T10:53:14.623 に答える