|
|
|
|
|
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.
|
|
|
|
|
|
## Current Proxy/Typeable Proposal (Apr 11, 2013)
|
|
|
## Current Proxy/Typeable Proposal (Apr 24, 2013)
|
|
|
|
|
|
|
|
|
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.
|
... | ... | @@ -29,25 +29,10 @@ instance Ord (a :=: b) where ... |
|
|
instance Category (:=:) where ...
|
|
|
-- what other instances?
|
|
|
|
|
|
data Void
|
|
|
-- instances as in Edward Kmett's 'void' package
|
|
|
|
|
|
absurd :: Void -> a
|
|
|
|
|
|
type Refuted a = a -> Void
|
|
|
data Decision a = Proved a
|
|
|
| Disproved (Refuted a)
|
|
|
|
|
|
class EqT f where
|
|
|
eqT :: f a -> f b -> Maybe (a :=: b)
|
|
|
|
|
|
class EqT f => DecideEqT f where
|
|
|
decideEqT :: f a -> f b -> Decision (a :=: b)
|
|
|
|
|
|
defaultEqT :: DecideEqT f => f a -> f b -> Maybe (a :=: b) -- for easy writing of EqT instances
|
|
|
|
|
|
instance EqT ((:=:) a) where ...
|
|
|
instance DecideEqT ((:=:) a) where ...
|
|
|
```
|
|
|
|
|
|
```wiki
|
... | ... | @@ -172,6 +157,26 @@ class (kparam ~ KindParam) => SingKind (kparam :: OfKind k) where |
|
|
|
|
|
- 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...
|
|
|
|
|
|
- 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!
|
|
|
|
|
|
```wiki
|
|
|
data Void
|
|
|
-- instances as in Edward Kmett's 'void' package
|
|
|
|
|
|
absurd :: Void -> a
|
|
|
|
|
|
type Refuted a = a -> Void
|
|
|
data Decision a = Proved a
|
|
|
| Disproved (Refuted a)
|
|
|
|
|
|
class EqT f => DecideEqT f where
|
|
|
decideEqT :: f a -> f b -> Decision (a :=: b)
|
|
|
|
|
|
defaultEqT :: DecideEqT f => f a -> f b -> Maybe (a :=: b) -- for easy writing of EqT instances
|
|
|
|
|
|
instance DecideEqT ((:=:) a) where ...
|
|
|
```
|
|
|
|
|
|
## Other thoughts (Gabor)
|
|
|
|
|
|
- Ultimately we want GHC to derive the `SingEquality` instance (`sameSing`, `decideSing` methods) for any singleton instance. GHC libraries should be laid out in a way that GHC's deriving engine can access all vital parts. IISC, this criterion rules out a completely detached library.
|
... | ... | |