次のように私はタイプレベルの論理和を定義したタイプレベルの論理和

Question

の冪等証明：

{-# LANGUAGE DataKinds, TypeFamilies #-} 

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

を今私はそれが冪等であること（Haskellで）を証明したいと思います。つまり、私はタイプidに動作可能と等価である

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

と用語idempを構築したいです。 （明らかに、私はそれを例えばunsafeCoerceと定義することができますが、それは不正です。）

それは可能ですか？

Answer 1

あなたが求めているものはできませんが、全く同じようなものがあります。証明には型レベルブーリアンのケース分析が必要ですが、そのようなイベントが発生するようなデータはありません。修正は、シングルトンを介してそのような情報だけを含めることです。

最初に、idempのタイプがやや難読化されています。 a ~ bという制約は、同じものを2度だけ命名します。次typechecks：

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

（あなたはtはaが含まれていない制約a ~ tを持っている場合、それは例外がinstance宣言であるaためtを代用するのは良いことだ：。何もマッチしますインスタンスヘッドでaしたがって、たとえその事が明らかにtになっていなくてもインスタンスは起動しますが、私は逃げ出します。）

私が請求するidemqは、bに関する有用な情報がないため、定義できません。入手可能なデータはpで、唯一のデータは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がTrueまたはFalseに減少し、そしてローカルに悪化することはできませんが、それのうち手立てが

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

はありませんことを表示する方法はありません。実行時には、bが何らかの形で値を計算するブーリアンの1つであるという証拠が必要です。私たちはそのためたちがBooly bを知っている場合、我々はbが何であるかを教えてくれるケース分析を行うことができます

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

を歌いましょう。それぞれの場合はうまくいくでしょう。ここでは、p bを抽象化するのではなく、PolyKindsで定義された等価タイプを使用して、ファクトをパックする方法について説明します。

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は、暗黙のうちにtypを修正するのに必要なOr b b ~ bの証拠を詰めています。 es。

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

Richard EisenbergとStephanie Weirichは、これらのファミリとクラスを作成するTemplate Haskellライブラリを用意しています。 SHEは、あまりにもそれらを構築し、あなたはpi b :: Bool.がforall b :: Bool. Booly b ->に展開

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

を書き込むことができますすることができます。

しかし、それはそのようなpalaverです。だから私のギャングは、実際にpiをHaskellに追加することに取り組んでいます。ノンパラメトリック量子（forallと->とは異なります）は、Haskellのタイプと用語の言語の間の重要でない交差点のものでインスタンス化できます。このpiには、引数がデフォルトで非表示になっている「暗黙の」変種もあります。 2つはそれぞれシングルトンファミリとクラスを使用することに対応していますが、追加のキットを入手するためにデータ型を3回以上定義する必要はありません。

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

Answer 2

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

典型的な溶液は、シングルトン型を使用して用語レベルでBool種類の構造を反映することである：任意b :: Boolについて

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

、SBool b（もちろんモジュロundefined）のほんの一住人があります。 SBoolで

は、定理を証明するのは簡単です（、あなたは余分な等式制約を追加した理由を私は知らない、私はそれを削除するつもりです）：

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

代わりに、明示的に引数を渡します、その後

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

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

：

あなたは SBool表現を作成できるクラスを定義することによって、暗黙のうちにそれを渡すことができます10

CBoolという制約を取り除くことはできませんが、a :: Boolではほとんど当てはまりませんので、あまり強い前提はありません。