Wie kann ich widersprüchliche Beweise verwenden?

Question

Während ich about how to do subtyping in Haskell schrieb, fiel mir auf, dass es sehr bequem wäre, widersprüchliche Beweise wie True ~ False zu "verwenden", um den Compiler über tote Zweige zu informieren. Mit einem weiteren Standard leer Typ, Void, die EmptyCase Erweiterung ermöglicht es Ihnen, einen toten Zweig zu markieren (dh eine, die einen Wert vom Typ enthält Void) auf diese Weise:

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

Ich mag würde etwas ähnliches für unerfüllbar Constraint tun s.

Gibt es einen Begriff, der den Typ True ~ False => a erhalten kann, aber nicht den Typ a erhalten kann?

Answer 1

Sie können dies oft tun, indem Sie die genaue Art der Beweise von der Art trennen, wie Sie sie verwenden möchten. Wenn der Typüberprüfer sieht, dass Sie eine absurde Einschränkung eingeführt haben, wird es Sie bellen. Der Trick besteht also darin, diese Gleichheit hinter :~: zu verzögern und dann den Gleichheitsnachweis mit allgemein vernünftigen Funktionen zu manipulieren.

{-# 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 

Die whoop Funktion scheint in etwa das, was Sie suchen.

---

Als András Kovács kommentiert, könnten Sie sogar EmptyCase auf dem 'False :~: 'True Wert verwenden nur. Derzeit (7.10.3) leider EmptyCasedoesn't warn about non-exhaustive matches. Dies wird hoffentlich bald behoben sein.

Answer 2

Eine solche Einschränkung führt zu einem Typfehler, wenn sie jemals als gegebene Einschränkung erscheint. Im Allgemeinen gilt dies für jede Einschränkung, die der Typchecker für unmöglich hält.

Schreiben auch eine Funktion

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

nicht funktioniert typecheck, weil der Kontext einer Funktion eine bestimmte Einschränkung im Körper der Funktion ist - und 'True ~ 'False einfach nicht als gegebene Einschränkung erscheinen.

Im besten Fall könnten Sie z.B.

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{} 

wieder, die auf dem :~: zurück zu einem EmptyCase, diesmal kommt. Beachten Sie, dass

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

auch ein trivialer unmöglich Einschränkung reduziert sich auf, weil x == x zu True reduziert. Sie könnten einen Gleichheitsvergleich schreiben, die nicht für trivialerweise gleich Typen nicht reduziert (zB die man in Data.Type.Equality), die Sie schreiben kann:

import Data.Type.Equality 

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

es eine Möglichkeit sein kann, diese Funktion ohne undefined zu schreiben, aber es ist Art strittig sowieso, da diese Art sofort von GHC reduziert:

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

ohne den Zwang

dort Auch ist es definitions unmöglich die Funktion Proxy '(y,y) -> a mit zwei verschiedenen anrufen Arten. Es gibt keine Möglichkeit, eine Gleichheitsbedingung ~ aus dem Typchecker auszublenden - Sie müssen eine andere Form der Gleichheit verwenden, eine, die nicht auf ~ reduziert wird.