どのように矛盾した証拠を使用できますか？

Question

about how to do subtyping in Haskellと書いているうちに、True ~ Falseなどの矛盾した証拠を "使用して"コンパイラに死んだブランチを知らせることができれば非常に便利だと私には気付きました。

use :: Void -> a 
use x = case x of 

は、私がConstraint充足不能のために類似した何かをしたいと思います：別の標準の空のタイプ、Voidで、EmptyCase拡張機能は、あなたがこの方法（タイプVoidの値が含まれているすなわち1）枯れ枝をマークすることができますs。

タイプはTrue ~ False => aとすることができますが、タイプはaではありませんか？

Answer 1

エビデンスの正確な性質を使用する方法から分離することで、これを行うことがよくあります。型式チェッカーが、あなたが不条理な制約を導入したと見なす場合、それはあなたに吠えます。だから、その均等性を:~:の後ろに遅らせ、一般的に合理的な関数を使って等価証拠を操作するのがこのトリックです。

{-# LANGUAGE GADTs, TypeOperators, ScopedTypeVariables, DataKinds, 
     PolyKinds, RankNTypes #-} 
{-# OPTIONS_GHC -Wall #-} 

module TrueFalse where 
import Data.Type.Equality 

data Foo (a :: Bool) where 
    Can :: Foo 'False 
    Can't :: (forall x . x) -> Foo 'True 

extr :: Foo 'True -> a 
extr (Can't x) = x 

subst :: a :~: b -> f a -> f b 
subst Refl x = x 

whoop :: 'False :~: 'True -> a 
whoop pf = extr $ subst pf Can 

whoop機能はお探しのものとほぼ同じです。アンドラス・コバックスとして

---

あなたもちょうど'False :~: 'True値にEmptyCaseを使用することができ、コメントしています。現在（7.10.3）、残念ながら、EmptyCasedoesn't warn about non-exhaustive matches。これは間もなく修正されることがうまくいくでしょう。

Answer 2

このような制約は、指定された制約として現れた場合に型エラーを引き起こします。一般に、これは、型式チェッカが不可能と判断する制約に適用されます。

がさえ

f :: ('True ~ 'False) => x 
f = undefined 

関数を作成することは、関数のコンテキストは、関数の本体で与えられた制約であるため、です。TypeCheckていない - と'True ~ 'Falseは、単に与えられた制約として表示することはできません。

再びEmptyCaseに来る

import Data.Type.Equality ((:~:)(..)) 

type family (==) (a :: k) (b :: k) :: Bool where 
    a == a = 'True 
    a == b = 'False 

f :: ((x == y) ~ 'False) => x :~: y -> a 
-- f Refl = undefined -- Inaccessible code 
f = \case{} 

、:~:でこの時間。 x == xがTrueに減少するので、

f :: ((x == y) ~ 'False, x ~ y) => a 

も自明不可能制約を減少させることに注意してください。 undefinedせずにこの関数を記述するための方法があるかもしれません

import Data.Type.Equality 

f :: ((x == y) ~ 'False, x ~ y) => Proxy '(x,y) -> a 
f = undefined 

が、それは次のとおりです。あなたが書くことができます自明同じ種類（Data.Type.Equalityで例えば1）のために減少しない等価述語を、書くことができますとにかく議論の余地の並べ替え、このタイプはすぐにGHCによって低減されるので：

>:t f 
f :: forall (k :: BOX) (y :: k) a. ((y == y) ~ 'False) => Proxy '(y, y) -> a 

でもそこ制約なしに、異なる2と機能Proxy '(y,y) -> aを呼び出すことdefinitionallyことは不可能ですタイプ。型チェックから平等制約~を隠す方法はありません。異なる型の等価を使用する必要があります。等しい型は~に縮小されません。