RFC: Singleton equality witnesses
Gabor Greif
ggreif at gmail.com
Wed Feb 6 19:03:43 CET 2013
On 2/5/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> I'm glad you've revived the thread, Gabor. My attention has been diverted
> elsewhere, but it's good to move forward with this. Thanks.
Hi Richard,
thanks for the encouragement!
>
> My argument would be not to return
> Maybe (SameSing kparam a b)
> but to return
> Either (SameSing kparam a b) (SameSing kparam a b -> Void)
> or something similar. (Void is taken from the void package, but it could
I see where you want to get at and recognize the added value. I have
two thoughts to add, though.
o most people are comfortable with assembling equality evidence (for
example by means of the Maybe monad), but few have done this for its
refutations.
o sometimes an equality proof is just what you need to proceed,
which is probably a smaller data structure to be created (laziness may
help here, but still allocates).
So I decided to leave 'sameSing' in and add a new method 'decideSing'
with your semantics. However, I have no idea how to implement the
non-equality pieces of Nat and Symbol. I have punted for now, failing
to add the corresponding branches. Maybe you can come up with
something sensible. Anyway, sameSing now has a default method that
maps positive evidence from decideSing into the Maybe monad.
I also flipped the type arguments to Either, since 'Right' sounds like
"Yep" and should signify positive evidence. I believe the ErrorT monad
transformer also uses this convention. (This is not a political
message, though :-)
> easily be redefined into any empty type.) You're right that empty pattern
> matches are available now (thanks, Simon!) but their usefulness comes into
> play only with the Either type, not with the Maybe type. What you have below
> would certainly be useful, but in my opinion, the Either construction is
> more so.
>
> Also, why generalize the return type with SameSing? Do you have a case where
> you would want the equality witness type to be other than (:~:)?
This leaves open the possibility of non-constructivistic evidence (is
there such a thing?). For example I could imagine an infinite Nat-like
type (with different representation) where we have a refutation proof
that n < m-1 and a refutation of n > m+1, and this would allow us to
construct evidence for n=m. I have seen
http://queuea9.wordpress.com/2012/11/05/canonize-this/ (and more
recent ones).
>
> I've thrown together a wiki page at
> http://hackage.haskell.org/trac/ghc/wiki/TypeLevelReasoning with Gabor's
> code, my code, and some of my thoughts. Please add your thoughts and any
> ideas into the mix!
I have commented on PropNot, suggesting alternatives.
Okay, here is the diff that I have so far:
-------------------------------------------------------------------
index f8b759e..7715a32 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -3,6 +3,7 @@
{-# LANGUAGE TypeFamilies #-} -- for declaring operators +
sing family
{-# LANGUAGE TypeOperators #-} -- for declaring operator
{-# LANGUAGE EmptyDataDecls #-} -- for declaring the kinds
+{-# LANGUAGE EmptyCase #-} -- for absurd
{-# LANGUAGE GADTs #-} -- for examining type nats
{-# LANGUAGE PolyKinds #-} -- for Sing family
{-# LANGUAGE FlexibleContexts #-}
@@ -30,7 +31,7 @@ module GHC.TypeLits
, type (-)
-- * Comparing for equality
- , type (:~:) (..), eqSingNat, eqSingSym
+ , type (:~:) (..), eqSingNat, eqSingSym, SingEquality (..)
-- * Destructing type-nat singletons.
, isZero, IsZero(..)
@@ -56,6 +57,8 @@ import Unsafe.Coerce(unsafeCoerce)
-- import Data.Bits(testBit,shiftR)
import Data.Maybe(Maybe(..))
import Data.List((++))
+import Data.Either(Either (..))
+import Control.Monad (guard, return, (>>))
-- | (Kind) A kind useful for passing kinds as parameters.
data OfKind (a :: *) = KindParam
@@ -133,6 +136,15 @@ class (kparam ~ KindParam) => SingE (kparam ::
OfKind k) where
type DemoteRep kparam :: *
fromSing :: Sing (a :: k) -> DemoteRep kparam
+class (kparam ~ KindParam, SingE (kparam :: OfKind k)) =>
SingEquality (kparam :: OfKind k) where
+ type SameSing kparam :: k -> k -> *
+ type SameSing kparam = (:~:)
+ sameSing :: Sing a -> Sing b -> Maybe (SameSing kparam a b)
+ sameSing a b = case decideSing a b of
+ Right witness -> Just witness
+ otherwise -> Nothing
+ decideSing :: Sing a -> Sing b -> Decision (SameSing kparam a b)
+
instance SingE (KindParam :: OfKind Nat) where
type DemoteRep (KindParam :: OfKind Nat) = Integer
fromSing (SNat n) = n
@@ -141,6 +153,16 @@ instance SingE (KindParam :: OfKind Symbol) where
type DemoteRep (KindParam :: OfKind Symbol) = String
fromSing (SSym s) = s
+instance SingEquality (KindParam :: OfKind Nat) where
+ sameSing = eqSingNat
+ decideSing a b = case eqSingNat a b of
+ Just witness -> Right witness
+
+instance SingEquality (KindParam :: OfKind Symbol) where
+ sameSing = eqSingSym
+ decideSing a b = case eqSingSym a b of
+ Just witness -> Right witness
+
{- | A convenient name for the type used to representing the values
for a particular singleton family. For example, @Demote 2 ~ Integer@,
and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String at . -}
@@ -236,6 +258,18 @@ data (:~:) :: k -> k -> * where
instance Show (a :~: b) where
show Refl = "Refl"
+
+-- | A type that has no inhabitants.
+data Void
+
+-- | Anything follow from falseness.
+absurd :: Void -> a
+absurd x = case x of {}
+
+type Refuted a = a -> Void
+
+type Decision a = Either (Refuted a) a
+
{- | Check if two type-natural singletons of potentially different types
are indeed the same, by comparing their runtime representations.
-------------------------------------------------------------------
I haven't exported all parts yet.
What do you think?
Cheers,
Gabor
>
> Richard
>
> On Feb 5, 2013, at 1:34 PM, Gabor Greif <ggreif at gmail.com> wrote:
>
>> Richard and all,
>>
>> sorry for reviving such an ancient thread, but I'd like to move this
>> forward a bit :-)
>>
>> In the meantime Iavor has added the (:~:) GADT, so I can reuse it. It
>> has been commented that it could (finally) end up in GHC.Exts, but for
>> now I want my changes minimized.
>>
>> I have added the class @SingEquality@ and have implemented the
>> @sameSing@ method in terms of Iavor's functions. This is rather pretty
>> now. Here is the patch:
>>
>> ------------------------------------------------------
>> $ git show 0eacf265255b9c5e0191b6a5100f3076b8eb5520
>> commit 0eacf265255b9c5e0191b6a5100f3076b8eb5520
>> Author: Gabor Greif <ggreif at gmail.com>
>> Date: Fri Nov 30 12:23:28 2012 +0100
>>
>> Introduce the SingEquality class
>> with customizable witness type
>> and a sameSing method that may
>> produce the latter.
>>
>> diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
>> index f8b759e..5546a5a 100644
>> --- a/GHC/TypeLits.hs
>> +++ b/GHC/TypeLits.hs
>> @@ -30,7 +30,7 @@ module GHC.TypeLits
>> , type (-)
>>
>> -- * Comparing for equality
>> - , type (:~:) (..), eqSingNat, eqSingSym
>> + , type (:~:) (..), eqSingNat, eqSingSym, SingEquality (..)
>>
>> -- * Destructing type-nat singletons.
>> , isZero, IsZero(..)
>> @@ -56,6 +56,7 @@ import Unsafe.Coerce(unsafeCoerce)
>> -- import Data.Bits(testBit,shiftR)
>> import Data.Maybe(Maybe(..))
>> import Data.List((++))
>> +import Control.Monad (guard, return, (>>))
>>
>> -- | (Kind) A kind useful for passing kinds as parameters.
>> data OfKind (a :: *) = KindParam
>> @@ -133,6 +134,11 @@ class (kparam ~ KindParam) => SingE (kparam ::
>> OfKind k) where
>> type DemoteRep kparam :: *
>> fromSing :: Sing (a :: k) -> DemoteRep kparam
>>
>> +class (kparam ~ KindParam, SingE (kparam :: OfKind k)) =>
>> SingEquality (kparam :: OfKind k) where
>> + type SameSing kparam :: k -> k -> *
>> + type SameSing kparam = (:~:)
>> + sameSing :: Sing a -> Sing b -> Maybe (SameSing kparam a b)
>> +
>> instance SingE (KindParam :: OfKind Nat) where
>> type DemoteRep (KindParam :: OfKind Nat) = Integer
>> fromSing (SNat n) = n
>> @@ -141,6 +147,12 @@ instance SingE (KindParam :: OfKind Symbol) where
>> type DemoteRep (KindParam :: OfKind Symbol) = String
>> fromSing (SSym s) = s
>>
>> +instance SingEquality (KindParam :: OfKind Nat) where
>> + sameSing = eqSingNat
>> +
>> +instance SingEquality (KindParam :: OfKind Symbol) where
>> + sameSing = eqSingSym
>> +
>> {- | A convenient name for the type used to representing the values
>> for a particular singleton family. For example, @Demote 2 ~ Integer@,
>> and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String at . -}
>> ------------------------------------------------------
>>
>> Regarding Richard's decidable equality suggestion, I think this would
>> be the next step. IIRC, empty case expressions have been implemented,
>> so GHC HEAD should be prepared.
>>
>> What do you think? Okay to push in this form?
>>
>> Cheers,
>>
>> Gabor
>>
>>
>> On 12/5/12, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>>> I don't think anything here is *high priority*, just musings on how best
>>> to
>>> move forward.
>>>
>>> About empty case, consider this:
>>>
>>>> data a :~: b where
>>>> Refl :: a :~: a
>>>>
>>>> absurd :: True :~: False -> a
>>>
>>> Now, I want to write a term binding for absurd. GHC can figure out that
>>> (True :~: False) is an empty type. So, if we have (absurd x = case x of
>>> …),
>>> there are no valid patterns, other than _, that could be used. Instead
>>> of
>>> writing (absurd _ = undefined), I would much prefer to write (absurd x =
>>> case x of {}). Why? If I compile with -fwarn-incomplete-patterns and
>>> -Werror, then the latter has no possible source of partiality and yet
>>> compiles. The former looks dangerous, and GHC doesn't check to make sure
>>> that, in fact, the function can never get called.
>>>
>>> The bottom line, for me at least, is that I want to avoid the partial
>>> constructs (incomplete patterns, undefined, etc) in Haskell as much as
>>> possible, especially when I'm leveraging the type system to a high
>>> degree.
>>> The lack of empty case statements forces me to use undefined where it
>>> isn't
>>> really necessary.
>>>
>>> I'll leave it to others to comment on TypeRep, as I'm a little hazy
>>> there
>>> myself.
>>>
>>> Richard
>>>
>>>
>>
>
>
More information about the ghc-devs
mailing list