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