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}}}. |
| 1 | This 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 | |
| 5 | This 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 | {{{ |
| 8 | module Data.Type.Equality where |
| 9 | |
| 10 | data 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' |
| 14 | sym :: (a :=: b) -> (b :=: a) |
| 15 | trans :: (a :=: b) -> (b :=: c) -> (a :=: c) |
| 16 | coerce :: (a :=: b) -> a -> b |
| 17 | liftEq :: (a :=: b) -> (f a :=: f b) |
| 18 | liftEq2 :: (a :=: a') -> (b :=: b') -> (f a b :=: f a' b') |
| 19 | liftEq3 :: ... |
| 20 | liftEq4 :: ... |
| 21 | lower :: (f a :=: f b) -> a :=: b |
| 22 | |
| 23 | instance Eq (a :=: b) where ... |
| 24 | instance Show (a :=: b) where ... |
| 25 | instance Read (a :=: a) where ... |
| 26 | instance Ord (a :=: b) where ... |
| 27 | instance Category (:=:) where ... |
| 28 | -- what other instances? |
| 29 | |
| 30 | data Void |
| 31 | -- instances as in Edward Kmett's 'void' package |
| 32 | |
| 33 | absurd :: Void -> a |
| 34 | |
| 35 | type Refuted a = a -> Void |
| 36 | data Decision a = Proved a |
| 37 | | Disproved (Refuted a) |
| 38 | |
| 39 | class EqT f where |
| 40 | eqT :: f a -> f b -> Maybe (a :=: b) |
| 41 | |
| 42 | class EqT f => DecideEqT f where |
| 43 | decideEqT :: f a -> f b -> Decision (a :=: b) |
| 44 | |
| 45 | defaultEqT :: DecideEqT f => f a -> f b -> Maybe (a :=: b) -- for easy writing of EqT instances |
| 46 | |
| 47 | instance EqT ((:=:) a) where ... |
| 48 | instance DecideEqT ((:=:) a) where ... |
| 49 | }}} |
| 50 | |
| 51 | {{{ |
| 52 | module 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 | {{{ |
| 59 | module Data.Typeable ( … , Proxy(..), (:=:)(..) ) where |
| 60 | |
| 61 | ... |
| 62 | import GHC.TypeReasoning |
| 63 | import {-# SOURCE #-} Data.Proxy |
| 64 | |
| 65 | ... |
| 66 | eqTypeable :: (Typeable a, Typeable b) => Maybe (a :=: b) |
| 67 | decideEqTypeable :: (Typeable a, Typeable b) => Decision (a :=: b) |
| 68 | -- can't use EqT and DecideEqT because Typeable is in Constraint, not * |
| 69 | |
| 70 | gcast :: (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 | |
| 79 | This is a great question. The reason the Data.Type.Equality module is in base |
| 80 | is 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. |
| 82 | If {{{gcast}}} is in ''base'', {{{eqTypeable}}} can be implemented as {{{gcast Refl}}}. It seems a little strange to have something like {{{eqTypeable}}} |
| 83 | defined somewhere other than Data.Typeable, but there is no technical |
| 84 | restriction here. By moving {{{eqTypeable}}} out of Data.Typeable, then |
| 85 | it seems we can also move Data.Type.Equality out, too. |
| 86 | |
| 87 | What about Data.Proxy? {{{Proxy}}} is re-exported from Data.Typeable, but |
| 88 | it is not used in that module. The idea here is that there should be a |
| 89 | canonical type to pass to {{{typeRep}}}, and {{{Proxy}}} is that canonical |
| 90 | type. |
| 91 | |
| 92 | == Updating !TypeLits/singletons == |
| 95 | |
| 96 | Proposed update to GHC.!TypeLits, using the definitions above: |
| 97 | |
| 98 | {{{ |
| 99 | instance EqT (Sing :: Nat -> *) where |
| 100 | eqT = defaultEqT |
| 101 | instance 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 | |
| 109 | With these definitions, there's an even stronger argument for keeping {{{(:=:)}}} |
| 110 | in ''base'': these instances would have to be orphans otherwise. |
| 111 | |
| 112 | Separate from the introduction of these instances, I would argue that |
| 113 | {{{unsafeSingNat}}} and {{{unsafeSingSymbol}}} should be moved from |
| 114 | GHC.!TypeLits to GHC.!TypeLits.Internal, which would be a new exposed module. |
| 115 | These two functions are very unsafe indeed, and their inclusion in |
| 116 | GHC.!TypeLits seems to violate a design principle of separating out unsafe |
| 117 | code. (Note that the uses of {{{unsafeCoerce}}} in GHC.!TypeLits seem benign, |
| 118 | and I think they should stay where they are.) |
| 119 | |
| 120 | == Older proposals == |