Changes between Version 11 and Version 12 of TypeLevelReasoning
 Timestamp:
 Apr 24, 2013 1:31:27 PM (3 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeLevelReasoning
v11 v12 1 1 This page collects ideas about definitions to support typelevel (propositional) reasoning in Haskell programs. Much of the initial content comes from the threads "RFC: Singleton equality witnesses" and "Proxy and newtypeable" on the ghcdevs and libraries mailing lists. 2 2 3 == Current Proxy/Typeable Proposal (Apr 11, 2013) ==3 == Current Proxy/Typeable Proposal (Apr 24, 2013) == 4 4 5 5 This proposal was sent to ghcdevs and libraries under the subject "Proxy, new Typeable, and typelevel equality" on April 3, 2013. The version below has edits that incorporate the feedback from responses to that email. … … 28 28  what other instances? 29 29 30 data Void31  instances as in Edward Kmett's 'void' package32 33 absurd :: Void > a34 35 type Refuted a = a > Void36 data Decision a = Proved a37  Disproved (Refuted a)38 39 30 class EqT f where 40 31 eqT :: f a > f b > Maybe (a :=: b) 41 32 42 class EqT f => DecideEqT f where43 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 instances46 47 33 instance EqT ((:=:) a) where ... 48 instance DecideEqT ((:=:) a) where ...49 34 }}} 50 35 … … 162 147 * 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... 163 148 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 {{{ 152 data Void 153  instances as in Edward Kmett's 'void' package 154 155 absurd :: Void > a 156 157 type Refuted a = a > Void 158 data Decision a = Proved a 159  Disproved (Refuted a) 160 161 class EqT f => DecideEqT f where 162 decideEqT :: f a > f b > Decision (a :=: b) 163 164 defaultEqT :: DecideEqT f => f a > f b > Maybe (a :=: b)  for easy writing of EqT instances 165 166 instance DecideEqT ((:=:) a) where ... 167 }}} 168 164 169 == Other thoughts (Gabor) == 165 170