22

そのため、小さな Haskell の演習を通じて Curry-Howard を半分理解しようとする継続的な試みの中で、私はこの時点で行き詰まってしまいました。

{-# LANGUAGE GADTs #-}

import Data.Void

type Not a = a -> Void

-- | The type of type equality proofs, which can only be instantiated if a = b.
data Equal a b where
    Refl :: Equal a a

-- | Derive a contradiction from a putative proof of @Equal Int Char@.
intIsNotChar :: Not (Equal Int Char)
intIsNotChar intIsChar = ???

明らかに、型Equal Int Charには (非底部の) 居住者がいないため、意味的には関数が存在するはずabsurdEquality :: Equal Int Char -> aです...しかし、私の人生では、を使用する以外に書く方法がわかりませんundefined。

したがって、次のいずれかです。

  1. 何かが足りない、または
  2. これを不可能な作業にする言語のいくつかの制限があり、それが何であるかを理解することができませんでした.

答えは次のようなものだと思います。コンパイラはEqual、a = b を持たないコンストラクターがないという事実を利用できません。しかし、もしそうなら、何がそれを真実にするのでしょうか?

4

2 に答える 2

22

これは、Philip JFのソリューションの短いバージョンです。これは、依存型理論家が何年にもわたって方程式に反論してきた方法です。

type family Discriminate x
type instance Discriminate Int  = ()
type instance Discriminate Char = Void

transport :: Equal a b -> Discriminate a -> Discriminate b
transport Refl d = d

refute :: Equal Int Char -> Void
refute q = transport q ()

物事が異なることを示すために、明確な観察結果をもたらす計算コンテキストを提供することによって、それらが異なる動作をするのを捕らえる必要があります。Discriminateまさにそのようなコンテキストを提供します。2つのタイプを異なる方法で処理するタイプレベルのプログラムです。

undefinedこの問題を解決するために頼る必要はありません。トータルプログラミングでは、不可能な入力を拒否することがあります。利用可能な場合でもundefined、totalメソッドで十分な場合は使用しないことをお勧めします。totalメソッドは、何かが不可能である理由を説明し、タイプチェッカーが確認します。undefined単にあなたの約束を文書化します。確かに、この反論の方法は、ケース分析がその領域をカバーすることを保証しながら、エピグラムが「不可能なケース」を省く方法です。

refute計算動作に関しては、viatransportは必然的に厳密でqありq、空のコンテキストでヘッドノーマルフォームを計算できないことに注意してください。これは、そのようなヘッドノーマルフォームが存在しないためです（もちろん、計算によってタイプが保持されるため）。refute全体的な設定では、実行時に呼び出されることはないと確信しています。Haskellでは、少なくとも、それに対応する義務を負う前に、その議論が分岐したり、例外をスローしたりすることは確実です。のような怠惰なバージョン

absurdEquality e = error "you have a type error likely to cause big problems"

の毒性を無視し、eそうでない場合はタイプエラーがあることを通知します。私は好きです

absurdEquality e = e `seq` error "sue me if this happens"

正直な反論が大変な仕事に似ている場合。

于 2013-01-11T11:35:57.207 に答える
7

undefinedHaskellではすべてのタイプを使用することの問題が底に住んでいることを私は理解していません。私たちの言語は強く正規化されていません...あなたは間違ったものを探しています。 よく保存された例外ではなくEqual Int Char、タイプエラーが発生します。見る

{-# LANGUAGE GADTs, TypeFamilies #-}

data Equal a b where
    Refl :: Equal a a

type family Pick cond a b
type instance Pick Char a b = a
type instance Pick Int a b = b

newtype Picker cond a b = Picker (Pick cond a b)

pick :: b -> Picker Int a b
pick = Picker

unpick :: Picker Char a b -> a
unpick (Picker x) = x

samePicker :: Equal t1 t2 -> Picker t1 a b -> Picker t2 a b
samePicker Refl x = x

absurdCoerce :: Equal Int Char -> a -> b
absurdCoerce e x = unpick (samePicker e (pick x))

これを使用して、必要な関数を作成できます

absurdEquality e = absurdCoerce e ()

しかし、それはその計算ルールとして未定義の振る舞いを生み出します。 falseプログラムを中止するか、少なくとも永久に実行する必要があります。中止は、最小論理を加算しないことによって直感的な論理に変えることに似た計算規則です。正しい定義は

absurdEquality e = error "you have a type error likely to cause big problems"

タイトルの質問に関して：本質的にいいえ。私の知る限り、現在のHaskellでは型の不等式を実際的な方法で表現することはできません。型システムに今後の変更はこれをより良くすることにつながるかもしれません、しかし今のところ、私たちは平等を持っていますが不平等はありません。

于 2013-01-11T07:19:25.603 に答える