Changes between Version 9 and Version 10 of TypeLevelReasoning


Ignore:
Timestamp:
Apr 12, 2013 12:53:52 PM (12 months 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