Welcome to OStack Knowledge Sharing Community for programmer and developer-Open, Learning and Share
Welcome To Ask or Share your Answers For Others

Categories

0 votes
1.1k views
in Technique[技术] by (71.8m points)

haskell - How can I use contradictory evidence?

While writing about how to do subtyping in Haskell, it occurred to me that it would be very convenient to be able to "use" contradictory evidence such as True ~ False to inform the compiler about dead branches. With another standard empty type, Void, the EmptyCase extension allows you to mark a dead branch (i.e. one that contains a value of type Void) this way:

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

I'd like to do something similar for unsatisfiable Constraints.

Is there a term which can be given the type True ~ False => a but cannot be given the type a?

See Question&Answers more detail:os

与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…
Welcome To Ask or Share your Answers For Others

1 Answer

0 votes
by (71.8m points)

You can often do this by separating the exact nature of the evidence from the way you plan to use it. If the type checker sees that you've introduced an absurd constraint, it will bark at you. So the trick is to delay that equality behind :~:, and then to manipulate the equality evidence using generally reasonable functions.

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

The whoop function seems to be approximately what you're looking for.


As András Kovács commented, you could even just use EmptyCase on the 'False :~: 'True value. At present (7.10.3), unfortunately, EmptyCase doesn't warn about non-exhaustive matches. This will hopefully be fixed soon.

Update 2019: that bug has been fixed.


与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…
Welcome to OStack Knowledge Sharing Community for programmer and developer-Open, Learning and Share
Click Here to Ask a Question

...