Changes between Version 11 and Version 12 of TypeLevelReasoning


Ignore:
Timestamp:
Apr 24, 2013 1:31:27 PM (2 years ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeLevelReasoning

    v11 v12  
    11This 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.
    22
    3 == Current Proxy/Typeable Proposal (Apr 11, 2013) ==
     3== Current Proxy/Typeable Proposal (Apr 24, 2013) ==
    44
    55This 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.
     
    2828-- what other instances?
    2929
    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 
    3930class EqT f where
    4031 eqT :: f a -> f b -> Maybe (a :=: b)
    4132
    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 
    4733instance EqT ((:=:) a) where ...
    48 instance DecideEqT ((:=:) a) where ...
    4934}}}
    5035
     
    162147 * 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...
    163148
     149 * I wanted the following to be in Data.Type.Equality, but I think I'm the only one, so I've removed these definitions from the original proposal. If you want them, please do shout -- I'd love company!
     150
     151{{{
     152data Void
     153-- instances as in Edward Kmett's 'void' package
     154
     155absurd :: Void -> a
     156
     157type Refuted a = a -> Void
     158data Decision a = Proved a
     159                | Disproved (Refuted a)
     160
     161class EqT f => DecideEqT f where
     162 decideEqT :: f a -> f b -> Decision (a :=: b)
     163
     164defaultEqT :: DecideEqT f => f a -> f b -> Maybe (a :=: b) -- for easy writing of EqT instances
     165
     166instance DecideEqT ((:=:) a) where ...
     167}}}
     168
    164169== Other thoughts (Gabor) ==
    165170