Changes between Version 9 and Version 10 of TypeLevelReasoning


Ignore:
Timestamp:
Apr 12, 2013 12:53:52 PM (2 years ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeLevelReasoning

    v9 v10  
    1 This page collects ideas about definitions to support type-level (propositional) reasoning in Haskell programs. Much of the initial content comes from the thread "RFC: Singleton equality witnesses" on ghc-devs. Currently (Feb 2013), these ideas are implemented in {{{GHC.TypeLits}}}.
     1This page collects ideas about definitions to support type-level (propositional) reasoning in Haskell programs. Much of the initial content comes from the threads "RFC: Singleton equality witnesses" and "Proxy and new-typeable" on the ghc-devs and libraries mailing lists.
     2
     3== Current Proxy/Typeable Proposal (Apr 11, 2013) ==
     4
     5This proposal was sent to ghc-devs and libraries under the subject "Proxy, new Typeable, and type-level equality" on April 3, 2013. The version below has edits that incorporate the feedback from responses to that email.
     6
     7{{{
     8module Data.Type.Equality where
     9
     10data a :=: b where
     11 Refl :: a :=: a
     12
     13-- with credit to Conal Elliott for 'ty', Erik Hesselink & Martijn van Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif for 'type-eq'
     14sym :: (a :=: b) -> (b :=: a)
     15trans :: (a :=: b) -> (b :=: c) -> (a :=: c)
     16coerce :: (a :=: b) -> a -> b
     17liftEq :: (a :=: b) -> (f a :=: f b)
     18liftEq2 :: (a :=: a') -> (b :=: b') -> (f a b :=: f a' b')
     19liftEq3 :: ...
     20liftEq4 :: ...
     21lower :: (f a :=: f b) -> a :=: b
     22
     23instance Eq (a :=: b) where ...
     24instance Show (a :=: b) where ...
     25instance Read (a :=: a) where ...
     26instance Ord (a :=: b) where ...
     27instance Category (:=:) where ...
     28-- what other instances?
     29
     30data Void
     31-- instances as in Edward Kmett's 'void' package
     32
     33absurd :: Void -> a
     34
     35type Refuted a = a -> Void
     36data Decision a = Proved a
     37                | Disproved (Refuted a)
     38
     39class EqT f where
     40 eqT :: f a -> f b -> Maybe (a :=: b)
     41
     42class EqT f => DecideEqT f where
     43 decideEqT :: f a -> f b -> Decision (a :=: b)
     44
     45defaultEqT :: DecideEqT f => f a -> f b -> Maybe (a :=: b) -- for easy writing of EqT instances
     46
     47instance EqT ((:=:) a) where ...
     48instance DecideEqT ((:=:) a) where ...
     49}}}
     50
     51{{{
     52module Data.Proxy where
     53-- as in Ben Gamari's version [1]
     54}}}
     55
     56[1]: https://github.com/bgamari/packages-base/blob/proxy/Data/Proxy.hs
     57
     58{{{
     59module Data.Typeable ( … , Proxy(..), (:=:)(..) ) where
     60
     61...
     62import GHC.TypeReasoning
     63import {-# SOURCE #-} Data.Proxy
     64
     65...
     66eqTypeable :: (Typeable a, Typeable b) => Maybe (a :=: b)
     67decideEqTypeable :: (Typeable a, Typeable b) => Decision (a :=: b)
     68-- can't use EqT and DecideEqT because Typeable is in Constraint, not *
     69
     70gcast :: (Typeable a, Typeable b) => c a -> Maybe (c b) -- it is now polykinded
     71
     72{-# DEPRECATED gcast1 ... #-}
     73{-# DEPRECATED gcast2 ... #-}
     74...
     75}}}
     76
     77=== Why are all of these in ''base''? ===
     78
     79This is a great question. The reason the Data.Type.Equality module is in base
     80is so that it can be used in Data.Typeable for {{{eqTypeable}}}. Does
     81{{{eqTypeable}}} ''need'' to be in ''base''? No, I (Richard) don't think so.
     82If {{{gcast}}} is in ''base'', {{{eqTypeable}}} can be implemented as {{{gcast Refl}}}. It seems a little strange to have something like {{{eqTypeable}}}
     83defined somewhere other than Data.Typeable, but there is no technical
     84restriction here. By moving {{{eqTypeable}}} out of Data.Typeable, then
     85it seems we can also move Data.Type.Equality out, too.
     86
     87What about Data.Proxy? {{{Proxy}}} is re-exported from Data.Typeable, but
     88it is not used in that module. The idea here is that there should be a
     89canonical type to pass to {{{typeRep}}}, and {{{Proxy}}} is that canonical
     90type.
     91
     92== Updating !TypeLits/singletons ==
    293
    394See also [wiki:TypeNats].
     95
     96Proposed update to GHC.!TypeLits, using the definitions above:
     97
     98{{{
     99instance EqT (Sing :: Nat -> *) where
     100  eqT = defaultEqT
     101instance DecideEqT (Sing :: Nat -> *) where
     102  decideEqT (SNat m) (SNat n)
     103    | m == n    = Proved (unsafeCoerce Refl)
     104    | otherwise = Disproved (error "...")
     105
     106-- similar for Symbol
     107}}}
     108
     109With these definitions, there's an even stronger argument for keeping {{{(:=:)}}}
     110in ''base'': these instances would have to be orphans otherwise.
     111
     112Separate from the introduction of these instances, I would argue that
     113{{{unsafeSingNat}}} and {{{unsafeSingSymbol}}} should be moved from
     114GHC.!TypeLits to GHC.!TypeLits.Internal, which would be a new exposed module.
     115These two functions are very unsafe indeed, and their inclusion in
     116GHC.!TypeLits seems to violate a design principle of separating out unsafe
     117code. (Note that the uses of {{{unsafeCoerce}}} in GHC.!TypeLits seem benign,
     118and I think they should stay where they are.)
     119
     120== Older proposals ==
    4121
    5122Gabor Greif's proposal:
     
    8125class (kparam ~ KindParam, SingE (kparam :: OfKind k)) => SingEquality (kparam :: OfKind k) where
    9126  type SameSing kparam :: k -> k -> *
    10   type SameSing kparam = (:~:)
     127  type SameSing kparam = (:=:)
    11128  sameSing :: Sing a -> Sing b -> Maybe (SameSing kparam a b)
    12129
     
    21138
    22139{{{
    23 -- Void and absurd are borrowed from Edward Kmett's 'void' package:
    24 data Void
    25 absurd :: Void -> a
    26 absurd x = case x of {}
    27 
    28 type PropNot a = a -> Void
    29 
    30 type Decision a = Either a (PropNot a)
    31 
    32140class SingE kparam => SingEquality (kparam :: OfKind k) where
    33   sameSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
     141  sameSing   :: forall (a :: k) (b :: k). Sing a -> Sing b ->
     142  decideSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :=: b)
    34143}}}
    35144
    36145I (Richard) think that using {{{Decision}}} instead of {{{Maybe}}} allows tighter programs to be written, because programmers can escape from impossible situations using {{{absurd}}}. If {{{sameSing}}} returns only a {{{Maybe}}}, then a programmer gets no information usable at the type level when the two singletons do not equal.
    37 
    38 Other variations:
    39 
    40  * In Edward Kmett's ''void'' package, he uses a different definition of {{{Void}}}:
    41 {{{
    42 newtype Void = Void Void
    43 }}}
    44 I'm not sure of the advantages/disadvantages of the choice of representation here. My guess is that Edward did this so his absurd function could spin infinitely. With empty case, we don't need that.
    45 
    46  * I'm not at all happy with the name {{{PropNot}}}, but I wanted to reserve {{{Not}}} for Boolean equality, as a parallel to {{{not}}}. Please suggest something better. Gabor suggests {{{Falsified}}}, or even better {{{Refuted}}}.
    47146
    48147== Other thoughts (Richard) ==
     
    61160 * I don't love having the functions {{{unsafeSingNat}}} and {{{unsafeSingSymbol}}} in {{{GHC.TypeLits}}}. I envision a future where, some day, a programmer could statically declare that they avoid the partial features of Haskell (along the lines of Safe Haskell, but stricter). Having these functions here means that this module would not be safe. (I am not bothered by various uses of {{{unsafeCoerce}}} within the module -- those uses certainly seem safe to me.) Instead, I propose that we move them to {{{GHC.TypeLits.Unsafe}}}.
    62161
    63  * Perhaps we should move some of what we're discussing out of {{{GHC.TypeLits}}}. After all, {{{(:~:)}}} does not interact directly with singletons, and neither do some of the definitions I mentioned above. I'm at a bit of a loss for a name, though...
     162 * Perhaps we should move some of what we're discussing out of {{{GHC.TypeLits}}}. After all, {{{(:=:)}}} does not interact directly with singletons, and neither do some of the definitions I mentioned above. I'm at a bit of a loss for a name, though...
    64163
    65164== Other thoughts (Gabor) ==
     
    73172Richard (11 Feb 2013): I've just pushed a commit to the type-reasoning branch with a strawman proposal of a reorganization of these definitions. Specifically, this commit breaks !TypeLits into the following five files:
    74173
    75  - GHC.!TypeEq, which contains the definitions for (:~:), Void, Refuted, etc.
     174 - GHC.!TypeEq, which contains the definitions for (:=:), Void, Refuted, etc.
    76175 - GHC.Singletons, which contains the definitions about singletons in general, such as SingI and !SingEquality
    77176 - GHC.!TypeLits.Unsafe, which contains just unsafeSingNat and unsafeSingSymbol