Version 11 (modified by simonpj, 3 years ago) (diff) |
---|

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)

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.

module Data.Type.Equality where data a :=: b where Refl :: a :=: a -- 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' sym :: (a :=: b) -> (b :=: a) trans :: (a :=: b) -> (b :=: c) -> (a :=: c) coerce :: (a :=: b) -> a -> b liftEq :: (a :=: b) -> (f a :=: f b) liftEq2 :: (a :=: a') -> (b :=: b') -> (f a b :=: f a' b') liftEq3 :: ... liftEq4 :: ... lower :: (f a :=: f b) -> a :=: b instance Eq (a :=: b) where ... instance Show (a :=: b) where ... instance Read (a :=: a) where ... 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 ...

module Data.Proxy where -- as in Ben Gamari's version [1]

[1]: https://github.com/bgamari/packages-base/blob/proxy/Data/Proxy.hs

module Data.Typeable ( … , Proxy(..), (:=:)(..) ) where ... import GHC.TypeReasoning import {-# SOURCE #-} Data.Proxy ... eqTypeable :: (Typeable a, Typeable b) => Maybe (a :=: b) decideEqTypeable :: (Typeable a, Typeable b) => Decision (a :=: b) -- can't use EqT and DecideEqT because Typeable is in Constraint, not * gcast :: (Typeable a, Typeable b) => c a -> Maybe (c b) -- it is now polykinded {-# DEPRECATED gcast1 ... #-} {-# DEPRECATED gcast2 ... #-} ...

### Why are all of these in *base*?

This is a great question. The reason the Data.Type.Equality module is in base
is so that it can be used in Data.Typeable for `eqTypeable`. Does
`eqTypeable` *need* to be in *base*? No, I (Richard) don't think so.
If `gcast` is in *base*, `eqTypeable` can be implemented as `gcast Refl`. It seems a little strange to have something like `eqTypeable`
defined somewhere other than Data.Typeable, but there is no technical
restriction here. By moving `eqTypeable` out of Data.Typeable, then
it seems we can also move Data.Type.Equality out, too.

What about Data.Proxy? `Proxy` is re-exported from Data.Typeable, but
it is not used in that module. The idea here is that there should be a
canonical type to pass to `typeRep`, and `Proxy` is that canonical
type.

## Updating TypeLits/singletons

See also TypeNats.

Proposed update to GHC.TypeLits, using the definitions above:

instance EqT (Sing :: Nat -> *) where eqT = defaultEqT instance DecideEqT (Sing :: Nat -> *) where decideEqT (SNat m) (SNat n) | m == n = Proved (unsafeCoerce Refl) | otherwise = Disproved (error "...") -- similar for Symbol

With these definitions, there's an even stronger argument for keeping `(:=:)`
in *base*: these instances would have to be orphans otherwise.

Separate from the introduction of these instances, I would argue that
`unsafeSingNat` and `unsafeSingSymbol` should be moved from
GHC.TypeLits to GHC.TypeLits.Internal, which would be a new exposed module.
These two functions are very unsafe indeed, and their inclusion in
GHC.TypeLits seems to violate a design principle of separating out unsafe
code. (Note that the uses of `unsafeCoerce` in GHC.TypeLits seem benign,
and I think they should stay where they are.)

## Older proposals

Gabor Greif's proposal:

class (kparam ~ KindParam, SingE (kparam :: OfKind k)) => SingEquality (kparam :: OfKind k) where type SameSing kparam :: k -> k -> * type SameSing kparam = (:=:) sameSing :: Sing a -> Sing b -> Maybe (SameSing kparam a b) instance SingEquality (KindParam :: OfKind Nat) where sameSing = eqSingNat instance SingEquality (KindParam :: OfKind Symbol) where sameSing = eqSingSym

Richard Eisenberg's proposal:

class SingE kparam => SingEquality (kparam :: OfKind k) where sameSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> decideSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :=: b)

I (Richard) think that using `Decision` instead of `Maybe` allows tighter programs to be written, because programmers can escape from impossible situations using `absurd`. If `sameSing` returns only a `Maybe`, then a programmer gets no information usable at the type level when the two singletons do not equal.

## Other thoughts (Richard)

- The
*singletons*package contains these definitions:

data SingInstance (a :: k) where SingInstance :: SingRep a => SingInstance a class (kparam ~ KindParam) => SingKind (kparam :: OfKind k) where singInstance :: forall (a :: k). Sing a -> SingInstance a

`SingKind (KindParam :: OfKind k)` states that the kind `k` has an associated singleton. I think that's a better superclass for `SingEquality` than just `SingE`.

- I don't love having the functions
`unsafeSingNat`and`unsafeSingSymbol`in`GHC.TypeLits`. I envision a future where, some day, a programmer could statically declare that they avoid the partial features of Haskell (along the lines of Safe Haskell, but stricter). Having these functions here means that this module would not be safe. (I am not bothered by various uses of`unsafeCoerce`within the module -- those uses certainly seem safe to me.) Instead, I propose that we move them to`GHC.TypeLits.Unsafe`.

- 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...

## 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.

## Course of Implementation

Gabor: I have created a new branch `type-reasoning` and pushed everything I have so far to the `libraries/base` repo. Richard's mail summarizes what still needs to be done.

Richard (11 Feb 2013): I've just pushed a commit to the type-reasoning branch with a strawman proposal of a reorganization of these definitions. Specifically, this commit breaks TypeLits into the following five files:

- GHC.TypeEq, which contains the definitions for (:=:), Void, Refuted, etc.
- GHC.Singletons, which contains the definitions about singletons in general, such as SingI and SingEquality
- GHC.TypeLits.Unsafe, which contains just unsafeSingNat and unsafeSingSymbol
- GHC.TypeLits.Internals, which is necessary to get GHC.TypeLits.Unsafe to have access to the right internals; this module is not exported from the 'base' package
- GHC.TypeLits, which contains the definitions specific to type-level literals.

Some thoughts on this design:

- First off, why is TypeEq part of GHC?? Because we wish to write eqSingNat and eqSingSym in GHC.TypeLits, and that module rightly deserves to be part of GHC. I'm quite uncomfortable with this decision, and I even created a new git repo at [github.com/goldfirere/type-reasoning] to hold the definitions that eventually ended up in GHC.TypeEq. (The repo has nothing in it, now.) Perhaps the best resolution is to move eqSingNat and eqSingSym out of GHC.TypeLits and into an external package, but that seems silly in a different direction. (It is fully technically feasible, as those functions don't depend on any internals.) I would love some feedback here.
- Why is Singletons broken off? No strong reason here, but it seemed that the singletons-oriented definitions weren't solely related to type-level literals, so it seemed more natural this way.
- Making the Unsafe module was a little more principled, because those functions really are unsafe! They are quite useful, though, and should be available somewhere.
- Currently, the internals of GHC assign types like "0" the kind GHC.TypeLits.Nat, so Nat and Symbol
**must**remain in the GHC.TypeLits module. Unfortunately, the plumbing around GHC.TypeLits.Unsafe want Nat and Symbol to be defined in GHC.TypeLits.Internals. So, I created a TypeLits.hs-boot file to fix the problem. This is highly unsatisfactory, and if something like what I've done here sticks around, we should change the internals of GHC to use GHC.TypeLits.Internals.Nat, getting rid of the import cycle. - I've put in the decideSing function as discussed further up in this thread. Its implementation for Nat and Symbol must use unsafeCoerce, but that shouldn't be a surprise.

Unfortunately, the code doesn't compile now. This is because it needs SingI instances for, say, Sing 0. For a reason I have not explored, these instances are not available here, though they seem to be for code written outside of GHC. Iavor, any thoughts on this?

Please tear any of these ideas (or my whole commit) to shreds! It really is meant to be a strawman proposal, but committing these changes seemed the best way of communicating on possible set of design decisions.

## Background Material

Edwin Brady's explanation how this is done in Idris.