diff --git a/Data/Constraint.hs b/Data/Constraint.hs deleted file mode 100644 --- a/Data/Constraint.hs +++ /dev/null @@ -1,578 +0,0 @@ -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE EmptyDataDecls #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE Trustworthy #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE CPP #-} -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE RoleAnnotations #-} -#endif ------------------------------------------------------------------------------ --- | --- Module : Data.Constraint --- Copyright : (C) 2011-2014 Edward Kmett, --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett --- Stability : experimental --- Portability : non-portable --- --- @ConstraintKinds@ made type classes into types of a new kind, @Constraint@. --- --- @ --- 'Eq' :: * -> 'Constraint' --- 'Ord' :: * -> 'Constraint' --- 'Monad' :: (* -> *) -> 'Constraint' --- @ --- --- The need for this extension was first publicized in the paper --- --- --- --- by Ralf Lämmel and Simon Peyton Jones in 2005, which shoehorned all the --- things they needed into a custom 'Sat' typeclass. --- --- With @ConstraintKinds@ we can put into code a lot of tools for manipulating --- these new types without such awkward workarounds. ----------------------------------------------------------------------------- -module Data.Constraint - ( - -- * The Kind of Constraints - Constraint - -- * Dictionary - , Dict(Dict) - -- * Entailment - , (:-)(Sub) - , (\\) - , weaken1, weaken2, contract - , (&&&), (***) - , trans, refl - , top, bottom - -- * Dict is fully faithful - , mapDict - , unmapDict - -- * Reflection - , Class(..) - , (:=>)(..) - ) where -import Control.Monad -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 -import Control.Category -#endif -import Control.Applicative -import Data.Monoid -import Data.Complex -import Data.Ratio -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 -import Data.Data -#endif -import GHC.Prim (Constraint) - --- | Values of type @'Dict' p@ capture a dictionary for a constraint of type @p@. --- --- e.g. --- --- @ --- 'Dict' :: 'Dict' ('Eq' 'Int') --- @ --- --- captures a dictionary that proves we have an: --- --- @ --- instance 'Eq' 'Int --- @ --- --- Pattern matching on the 'Dict' constructor will bring this instance into scope. --- -data Dict :: Constraint -> * where - Dict :: a => Dict a -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 - deriving Typeable - - -instance (Typeable p, p) => Data (Dict p) where - gfoldl _ z Dict = z Dict - toConstr _ = dictConstr - gunfold _ z c = case constrIndex c of - 1 -> z Dict - _ -> error "gunfold" - dataTypeOf _ = dictDataType - -dictConstr :: Constr -dictConstr = mkConstr dictDataType "Dict" [] Prefix - -dictDataType :: DataType -dictDataType = mkDataType "Data.Constraint.Dict" [dictConstr] -#endif - -deriving instance Eq (Dict a) -deriving instance Ord (Dict a) -deriving instance Show (Dict a) - -infixr 9 :- - --- | This is the type of entailment. --- --- @a ':-' b@ is read as @a@ \"entails\" @b@. --- --- With this we can actually build a category for 'Constraint' resolution. --- --- e.g. --- --- Because @'Eq' a@ is a superclass of @'Ord' a@, we can show that @'Ord' a@ --- entails @'Eq' a@. --- --- Because @instance 'Ord' a => 'Ord' [a]@ exists, we can show that @'Ord' a@ --- entails @'Ord' [a]@ as well. --- --- This relationship is captured in the ':-' entailment type here. --- --- Since @p ':-' p@ and entailment composes, ':-' forms the arrows of a 'Category' --- of constraints. However, 'Category' only because sufficiently general to support this --- instance in GHC 7.8, so prior to 7.8 this instance is unavailable. --- --- But due to the coherence of instance resolution in Haskell, this 'Category' --- has some very interesting properties. Notably, in the absence of --- @IncoherentInstances@, this category is \"thin\", which is to say that --- between any two objects (constraints) there is at most one distinguishable --- arrow. --- --- This means that for instance, even though there are two ways to derive --- @'Ord' a ':-' 'Eq' [a]@, the answers from these two paths _must_ by --- construction be equal. This is a property that Haskell offers that is --- pretty much unique in the space of languages with things they call \"type --- classes\". --- --- What are the two ways? --- --- Well, we can go from @'Ord' a ':-' 'Eq' a@ via the --- superclass relationship, and them from @'Eq' a ':-' 'Eq' [a]@ via the --- instance, or we can go from @'Ord' a ':-' 'Ord' [a]@ via the instance --- then from @'Ord' [a] ':-' 'Eq' [a]@ through the superclass relationship --- and this diagram by definition must \"commute\". --- --- Diagrammatically, --- --- > Ord a --- > ins / \ cls --- > v v --- > Ord [a] Eq a --- > cls \ / ins --- > v v --- > Eq [a] --- --- This safety net ensures that pretty much anything you can write with this --- library is sensible and can't break any assumptions on the behalf of --- library authors. -newtype a :- b = Sub (a => Dict b) -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 - deriving Typeable - -type role (:-) nominal nominal - --- TODO: _proper_ Data for @(p ':-' q)@ requires @(:-)@ to be cartesian _closed_. --- --- This is admissable, but not present by default - --- constraint should be instance (Typeable p, Typeable q, p |- q) => Data (p :- q) -instance (Typeable p, Typeable q, p, q) => Data (p :- q) where - gfoldl _ z (Sub Dict) = z (Sub Dict) - toConstr _ = subConstr - gunfold _ z c = case constrIndex c of - 1 -> z (Sub Dict) - _ -> error "gunfold" - dataTypeOf _ = subDataType - -subConstr :: Constr -subConstr = mkConstr dictDataType "Sub" [] Prefix - -subDataType :: DataType -subDataType = mkDataType "Data.Constraint.:-" [subConstr] - --- | Possible since GHC 7.8, when 'Category' was made polykinded. -instance Category (:-) where - id = refl - (.) = trans -#endif - --- | Assumes 'IncoherentInstances' doesn't exist. -instance Eq (a :- b) where - _ == _ = True - --- | Assumes 'IncoherentInstances' doesn't exist. -instance Ord (a :- b) where - compare _ _ = EQ - -instance Show (a :- b) where - showsPrec d _ = showParen (d > 10) $ showString "Sub Dict" - -infixl 1 \\ -- required comment - --- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@ -(\\) :: a => (b => r) -> (a :- b) -> r -r \\ Sub Dict = r - --------------------------------------------------------------------------------- --- Constraints form a Category --------------------------------------------------------------------------------- - --- | Transitivity of entailment --- --- If we view @(':-')@ as a Constraint-indexed category, then this is @('.')@ -trans :: (b :- c) -> (a :- b) -> a :- c -trans f g = Sub $ Dict \\ f \\ g - --- | Reflexivity of entailment --- --- If we view @(':-')@ as a Constraint-indexed category, then this is 'id' -refl :: a :- a -refl = Sub Dict - --------------------------------------------------------------------------------- --- (,) is a Bifunctor --------------------------------------------------------------------------------- - --- | due to the hack for the kind of @(,)@ in the current version of GHC we can't actually --- make instances for @(,) :: Constraint -> Constraint -> Constraint@, but @(,)@ is a --- bifunctor on the category of constraints. This lets us map over both sides. -(***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d) -f *** g = Sub $ Dict \\ f \\ g - --------------------------------------------------------------------------------- --- Constraints are Cartesian --------------------------------------------------------------------------------- - --- | Weakening a constraint product --- --- The category of constraints is Cartesian. We can forget information. -weaken1 :: (a, b) :- a -weaken1 = Sub Dict - --- | Weakening a constraint product --- --- The category of constraints is Cartesian. We can forget information. -weaken2 :: (a, b) :- b -weaken2 = Sub Dict - --- | Contracting a constraint / diagonal morphism --- --- The category of constraints is Cartesian. We can reuse information. -contract :: a :- (a, a) -contract = Sub Dict - --- | Constraint product --- --- > trans weaken1 (f &&& g) = f --- > trans weaken2 (f &&& g) = g -(&&&) :: (a :- b) -> (a :- c) -> a :- (b, c) -f &&& g = Sub $ Dict \\ f \\ g - --------------------------------------------------------------------------------- --- Initial and terminal morphisms --------------------------------------------------------------------------------- - --- | Every constraint implies truth --- --- These are the terminal arrows of the category, and @()@ is the terminal object. --- --- Given any constraint there is a unique entailment of the @()@ constraint from that constraint. -top :: a :- () -top = Sub Dict - -type family Ex (a :: *) (c :: Constraint) :: Constraint -type instance Ex () c = () -type instance Ex Bool c = c - -falso :: (() ~ a) :- Ex a c -falso = Sub Dict - --- | --- A bad type coercion lets you derive any constraint you want. --- --- These are the initial arrows of the category and @(() ~ Bool)@ is the initial object --- --- This demonstrates the law of classical logic -bottom :: (() ~ Bool) :- c -bottom = falso - --------------------------------------------------------------------------------- --- Dict is fully faithful --------------------------------------------------------------------------------- - --- | Apply an entailment to a dictionary. --- --- From a category theoretic perspective 'Dict' is a functor that maps from the category --- of constraints (with arrows in ':-') to the category Hask of Haskell data types. -mapDict :: (a :- b) -> Dict a -> Dict b -mapDict p Dict = case p of Sub q -> q - --- | --- This functor is fully faithful, which is to say that given any function you can write --- @Dict a -> Dict b@ there also exists an entailment @a :- b@ in the category of constraints --- that you can build. -unmapDict :: (Dict a -> Dict b) -> a :- b -unmapDict f = Sub (f Dict) - -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 -type role Dict nominal -#endif - --------------------------------------------------------------------------------- --- Reflection --------------------------------------------------------------------------------- - --- | Reify the relationship between a class and its superclass constraints as a class --- --- Given a definition such as --- --- @ --- class Foo a => Bar a --- @ --- --- you can capture the relationship between 'Bar a' and its superclass 'Foo a' with --- --- @ --- instance 'Class' (Foo a) (Bar a) where 'cls' = 'Sub' 'Dict' --- @ --- --- Now the user can use 'cls :: Bar a :- Foo a' -class Class b h | h -> b where - cls :: h :- b - -infixr 9 :=> --- | Reify the relationship between an instance head and its body as a class --- --- Given a definition such as --- --- @ --- instance Foo a => Foo [a] --- @ --- --- you can capture the relationship between the instance head and its body with --- --- @ --- instance Foo a ':=>' Foo [a] where 'ins' = 'Sub' 'Dict' --- @ -class b :=> h | h -> b where - ins :: b :- h - --- Bootstrapping - -instance Class () (Class b a) where cls = Sub Dict -instance Class () (b :=> a) where cls = Sub Dict - -instance Class b a => () :=> Class b a where ins = Sub Dict -instance (b :=> a) => () :=> b :=> a where ins = Sub Dict - -instance Class () () where cls = Sub Dict -instance () :=> () where ins = Sub Dict - --- Local, Prelude, Applicative, C.M.I and Data.Monoid instances - --- Eq -instance Class () (Eq a) where cls = Sub Dict -instance () :=> Eq () where ins = Sub Dict -instance () :=> Eq Int where ins = Sub Dict -instance () :=> Eq Bool where ins = Sub Dict -instance () :=> Eq Integer where ins = Sub Dict -instance () :=> Eq Float where ins = Sub Dict -instance () :=> Eq Double where ins = Sub Dict -instance Eq a :=> Eq [a] where ins = Sub Dict -instance Eq a :=> Eq (Maybe a) where ins = Sub Dict -instance Eq a :=> Eq (Complex a) where ins = Sub Dict -instance Eq a :=> Eq (Ratio a) where ins = Sub Dict -instance (Eq a, Eq b) :=> Eq (a, b) where ins = Sub Dict -instance (Eq a, Eq b) :=> Eq (Either a b) where ins = Sub Dict -instance () :=> Eq (Dict a) where ins = Sub Dict -instance () :=> Eq (a :- b) where ins = Sub Dict - --- Ord -instance Class (Eq a) (Ord a) where cls = Sub Dict -instance () :=> Ord () where ins = Sub Dict -instance () :=> Ord Bool where ins = Sub Dict -instance () :=> Ord Int where ins = Sub Dict -instance ():=> Ord Integer where ins = Sub Dict -instance () :=> Ord Float where ins = Sub Dict -instance ():=> Ord Double where ins = Sub Dict -instance () :=> Ord Char where ins = Sub Dict -instance Ord a :=> Ord (Maybe a) where ins = Sub Dict -instance Ord a :=> Ord [a] where ins = Sub Dict -instance (Ord a, Ord b) :=> Ord (a, b) where ins = Sub Dict -instance (Ord a, Ord b) :=> Ord (Either a b) where ins = Sub Dict -instance Integral a :=> Ord (Ratio a) where ins = Sub Dict -instance () :=> Ord (Dict a) where ins = Sub Dict -instance () :=> Ord (a :- b) where ins = Sub Dict - --- Show -instance Class () (Show a) where cls = Sub Dict -instance () :=> Show () where ins = Sub Dict -instance () :=> Show Bool where ins = Sub Dict -instance () :=> Show Ordering where ins = Sub Dict -instance () :=> Show Char where ins = Sub Dict -instance Show a :=> Show (Complex a) where ins = Sub Dict -instance Show a :=> Show [a] where ins = Sub Dict -instance Show a :=> Show (Maybe a) where ins = Sub Dict -instance (Show a, Show b) :=> Show (a, b) where ins = Sub Dict -instance (Show a, Show b) :=> Show (Either a b) where ins = Sub Dict -instance (Integral a, Show a) :=> Show (Ratio a) where ins = Sub Dict -instance () :=> Show (Dict a) where ins = Sub Dict -instance () :=> Show (a :- b) where ins = Sub Dict - --- Read -instance Class () (Read a) where cls = Sub Dict -instance () :=> Read () where ins = Sub Dict -instance () :=> Read Bool where ins = Sub Dict -instance () :=> Read Ordering where ins = Sub Dict -instance () :=> Read Char where ins = Sub Dict -instance Read a :=> Read (Complex a) where ins = Sub Dict -instance Read a :=> Read [a] where ins = Sub Dict -instance Read a :=> Read (Maybe a) where ins = Sub Dict -instance (Read a, Read b) :=> Read (a, b) where ins = Sub Dict -instance (Read a, Read b) :=> Read (Either a b) where ins = Sub Dict -instance (Integral a, Read a) :=> Read (Ratio a) where ins = Sub Dict - --- Enum -instance Class () (Enum a) where cls = Sub Dict -instance () :=> Enum () where ins = Sub Dict -instance () :=> Enum Bool where ins = Sub Dict -instance () :=> Enum Ordering where ins = Sub Dict -instance () :=> Enum Char where ins = Sub Dict -instance () :=> Enum Int where ins = Sub Dict -instance () :=> Enum Integer where ins = Sub Dict -instance () :=> Enum Float where ins = Sub Dict -instance () :=> Enum Double where ins = Sub Dict -instance Integral a :=> Enum (Ratio a) where ins = Sub Dict - --- Bounded -instance Class () (Bounded a) where cls = Sub Dict -instance () :=> Bounded () where ins = Sub Dict -instance () :=> Bounded Ordering where ins = Sub Dict -instance () :=> Bounded Bool where ins = Sub Dict -instance () :=> Bounded Int where ins = Sub Dict -instance () :=> Bounded Char where ins = Sub Dict -instance (Bounded a, Bounded b) :=> Bounded (a,b) where ins = Sub Dict - --- Num -instance Class () (Num a) where cls = Sub Dict -instance () :=> Num Int where ins = Sub Dict -instance () :=> Num Integer where ins = Sub Dict -instance () :=> Num Float where ins = Sub Dict -instance () :=> Num Double where ins = Sub Dict -instance RealFloat a :=> Num (Complex a) where ins = Sub Dict -instance Integral a :=> Num (Ratio a) where ins = Sub Dict - --- Real -instance Class (Num a, Ord a) (Real a) where cls = Sub Dict -instance () :=> Real Int where ins = Sub Dict -instance () :=> Real Integer where ins = Sub Dict -instance () :=> Real Float where ins = Sub Dict -instance () :=> Real Double where ins = Sub Dict -instance Integral a :=> Real (Ratio a) where ins = Sub Dict - --- Integral -instance Class (Real a, Enum a) (Integral a) where cls = Sub Dict -instance () :=> Integral Int where ins = Sub Dict -instance () :=> Integral Integer where ins = Sub Dict - --- Fractional -instance Class (Num a) (Fractional a) where cls = Sub Dict -instance () :=> Fractional Float where ins = Sub Dict -instance () :=> Fractional Double where ins = Sub Dict -instance RealFloat a :=> Fractional (Complex a) where ins = Sub Dict -instance Integral a :=> Fractional (Ratio a) where ins = Sub Dict - --- Floating -instance Class (Fractional a) (Floating a) where cls = Sub Dict -instance () :=> Floating Float where ins = Sub Dict -instance () :=> Floating Double where ins = Sub Dict -instance RealFloat a :=> Floating (Complex a) where ins = Sub Dict - --- RealFrac -instance Class (Real a, Fractional a) (RealFrac a) where cls = Sub Dict -instance () :=> RealFrac Float where ins = Sub Dict -instance () :=> RealFrac Double where ins = Sub Dict -instance Integral a :=> RealFrac (Ratio a) where ins = Sub Dict - --- RealFloat -instance Class (RealFrac a, Floating a) (RealFloat a) where cls = Sub Dict -instance () :=> RealFloat Float where ins = Sub Dict -instance () :=> RealFloat Double where ins = Sub Dict - --- Monoid -instance Class () (Monoid a) where cls = Sub Dict -instance () :=> Monoid () where ins = Sub Dict -instance () :=> Monoid Ordering where ins = Sub Dict -instance () :=> Monoid [a] where ins = Sub Dict -instance Monoid a :=> Monoid (Maybe a) where ins = Sub Dict -instance (Monoid a, Monoid b) :=> Monoid (a, b) where ins = Sub Dict - --- Functor -instance Class () (Functor f) where cls = Sub Dict -instance () :=> Functor [] where ins = Sub Dict -instance () :=> Functor Maybe where ins = Sub Dict -instance () :=> Functor (Either a) where ins = Sub Dict -instance () :=> Functor ((->) a) where ins = Sub Dict -instance () :=> Functor ((,) a) where ins = Sub Dict -instance () :=> Functor IO where ins = Sub Dict -instance Monad m :=> Functor (WrappedMonad m) where ins = Sub Dict - --- Applicative -instance Class (Functor f) (Applicative f) where cls = Sub Dict -instance () :=> Applicative [] where ins = Sub Dict -instance () :=> Applicative Maybe where ins = Sub Dict -instance () :=> Applicative (Either a) where ins = Sub Dict -instance () :=> Applicative ((->)a) where ins = Sub Dict -instance () :=> Applicative IO where ins = Sub Dict -instance Monoid a :=> Applicative ((,)a) where ins = Sub Dict -instance Monad m :=> Applicative (WrappedMonad m) where ins = Sub Dict - --- Alternative -instance Class (Applicative f) (Alternative f) where cls = Sub Dict -instance () :=> Alternative [] where ins = Sub Dict -instance () :=> Alternative Maybe where ins = Sub Dict -instance MonadPlus m :=> Alternative (WrappedMonad m) where ins = Sub Dict - --- Monad -instance Class () (Monad f) where cls = Sub Dict -instance () :=> Monad [] where ins = Sub Dict -instance () :=> Monad ((->) a) where ins = Sub Dict -instance () :=> Monad (Either a) where ins = Sub Dict -instance () :=> Monad IO where ins = Sub Dict - --- MonadPlus -instance Class (Monad f) (MonadPlus f) where cls = Sub Dict -instance () :=> MonadPlus [] where ins = Sub Dict -instance () :=> MonadPlus Maybe where ins = Sub Dict - --------------------------------------------------------------------------------- --- UndecidableInstances --------------------------------------------------------------------------------- - -instance a :=> Enum (Dict a) where ins = Sub Dict -instance a => Enum (Dict a) where - toEnum _ = Dict - fromEnum Dict = 0 - -instance a :=> Bounded (Dict a) where ins = Sub Dict -instance a => Bounded (Dict a) where - minBound = Dict - maxBound = Dict - -instance a :=> Read (Dict a) where ins = Sub Dict -deriving instance a => Read (Dict a) - -instance a :=> Monoid (Dict a) where ins = Sub Dict -instance a => Monoid (Dict a) where - mappend Dict Dict = Dict - mempty = Dict diff --git a/Data/Constraint/Forall.hs b/Data/Constraint/Forall.hs deleted file mode 100644 --- a/Data/Constraint/Forall.hs +++ /dev/null @@ -1,70 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE EmptyDataDecls #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE Trustworthy #-} -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 -{-# LANGUAGE RoleAnnotations #-} -#endif ------------------------------------------------------------------------------ --- | --- Module : Data.Constraint.Forall --- Copyright : (C) 2011-2013 Edward Kmett, --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett --- Stability : experimental --- Portability : non-portable --- --- This module uses a trick to provide quantification over constraints. ----------------------------------------------------------------------------- - -module Data.Constraint.Forall - ( Forall, inst - , ForallF, instF - , Forall1, inst1 - , ForallT, instT - ) where - -import Data.Constraint -import Data.Constraint.Unsafe - --- skolem variables, do not export! -data A -data B --- | A quantified constraint -type Forall (p :: * -> Constraint) = (p A, p B) - -type ForallF (p :: * -> Constraint) (f :: * -> *) = (p (f A), p (f B)) - -data F a -data M a - -type Forall1 (p :: (* -> *) -> Constraint) = (p F, p M) - -type ForallT (p :: * -> Constraint) (t :: (* -> *) -> * -> *) = (p (t F A), p (t M B)) - -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 -type role F nominal -type role M nominal -#endif - - --- | instantiate a quantified constraint on kind @*@ -inst :: forall p a. Forall p :- p a -inst = trans (unsafeCoerceConstraint :: p A :- p a) weaken1 - -instF :: forall p f a. ForallF p f :- p (f a) -instF = trans (unsafeCoerceConstraint :: p (f A) :- p (f a)) weaken1 - --- | instantiate a quantified constraint on kind @* -> *@ -inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall1 p :- p f -inst1 = trans (unsafeCoerceConstraint :: p F :- p f) weaken1 - -instT :: forall (p :: * -> Constraint) (t :: (* -> *) -> * -> *) (f :: * -> *) a. ForallT p t :- p (t f a) -instT = trans (unsafeCoerceConstraint :: p (t F A) :- p (t f a)) weaken1 - diff --git a/Data/Constraint/Unsafe.hs b/Data/Constraint/Unsafe.hs deleted file mode 100644 --- a/Data/Constraint/Unsafe.hs +++ /dev/null @@ -1,55 +0,0 @@ -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE EmptyDataDecls #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE Unsafe #-} ------------------------------------------------------------------------------ --- | --- Module : Data.Constraint.Unsafe --- Copyright : (C) 2011-2013 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett --- Stability : experimental --- Portability : non-portable --- ----------------------------------------------------------------------------- -module Data.Constraint.Unsafe - ( unsafeCoerceConstraint - , unsafeDerive - , unsafeUnderive - -- * Sugar - , unsafeApplicative - , unsafeAlternative - ) where - -import Control.Applicative -import Control.Monad -import Control.Newtype -import Data.Constraint -import Unsafe.Coerce - --- | Coerce a dictionary unsafely from one type to another -unsafeCoerceConstraint :: a :- b -unsafeCoerceConstraint = unsafeCoerce refl - --- | Coerce a dictionary unsafely from one type to a newtype of that type -unsafeDerive :: Newtype n o => (o -> n) -> t o :- t n -unsafeDerive _ = unsafeCoerceConstraint - --- | Coerce a dictionary unsafely from a newtype of a type to the base type -unsafeUnderive :: Newtype n o => (o -> n) -> t n :- t o -unsafeUnderive _ = unsafeCoerceConstraint - --- | Construct an Applicative instance from a Monad -unsafeApplicative :: forall m a. Monad m => (Applicative m => m a) -> m a -unsafeApplicative m = m \\ trans (unsafeCoerceConstraint :: Applicative (WrappedMonad m) :- Applicative m) ins - --- | Construct an Alternative instance from a MonadPlus -unsafeAlternative :: forall m a. MonadPlus m => (Alternative m => m a) -> m a -unsafeAlternative m = m \\ trans (unsafeCoerceConstraint :: Alternative (WrappedMonad m) :- Alternative m) ins diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright 2011-2013 Edward Kmett +Copyright 2011-2015 Edward Kmett All rights reserved. diff --git a/constraints.cabal b/constraints.cabal --- a/constraints.cabal +++ b/constraints.cabal @@ -1,6 +1,6 @@ name: constraints category: Constraints -version: 0.4.1.3 +version: 0.6 license: BSD3 cabal-version: >= 1.10 license-file: LICENSE @@ -9,7 +9,7 @@ stability: experimental homepage: http://github.com/ekmett/constraints/ bug-reports: http://github.com/ekmett/constraints/issues -copyright: Copyright (C) 2011-2014 Edward A. Kmett +copyright: Copyright (C) 2011-2015 Edward A. Kmett synopsis: Constraint manipulation description: GHC 7.4 gave us the ability to talk about @ConstraintKinds@. They stopped crashing the compiler in GHC 7.6. @@ -17,7 +17,7 @@ This package provides a vocabulary for working with them. build-type: Simple -tested-with: GHC == 7.8.3, GHC == 7.7.20131027, GHC == 7.7.20131025, GHC == 7.6.3 +tested-with: GHC == 7.8.3, GHC == 7.7.20131027, GHC == 7.7.20131025 extra-source-files: README.markdown source-repository head @@ -25,6 +25,8 @@ location: git://github.com/ekmett/constraints.git library + hs-source-dirs: src + default-language: Haskell2010 other-extensions: FunctionalDependencies, @@ -39,12 +41,27 @@ GADTs build-depends: - base >= 4.5 && < 5, - newtype >= 0.2 && < 0.3, - ghc-prim + base >= 4.6 && < 5, + binary >= 0.7.3 && < 0.8, + deepseq >= 1.3 && < 1.5, + ghc-prim, + hashable >= 1.2 && < 1.3, + mtl >= 2 && < 2.3, + transformers >= 0.2 && < 0.5, + transformers-compat >= 0.4 && < 1 + + if impl(ghc < 7.8) + build-depends: + newtype >= 0.2 && < 0.3, + tagged >= 0.2 && < 1 + else + exposed-modules: + Data.Constraint.Forall + exposed-modules: Data.Constraint - Data.Constraint.Forall + Data.Constraint.Deferrable + Data.Constraint.Lifting Data.Constraint.Unsafe ghc-options: -Wall diff --git a/src/Data/Constraint.hs b/src/Data/Constraint.hs new file mode 100644 --- /dev/null +++ b/src/Data/Constraint.hs @@ -0,0 +1,580 @@ +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE CPP #-} +#if __GLASGOW_HASKELL__ >= 707 +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE RoleAnnotations #-} +#endif +----------------------------------------------------------------------------- +-- | +-- Module : Data.Constraint +-- Copyright : (C) 2011-2015 Edward Kmett, +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Edward Kmett +-- Stability : experimental +-- Portability : non-portable +-- +-- @ConstraintKinds@ made type classes into types of a new kind, @Constraint@. +-- +-- @ +-- 'Eq' :: * -> 'Constraint' +-- 'Ord' :: * -> 'Constraint' +-- 'Monad' :: (* -> *) -> 'Constraint' +-- @ +-- +-- The need for this extension was first publicized in the paper +-- +-- +-- +-- by Ralf Lämmel and Simon Peyton Jones in 2005, which shoehorned all the +-- things they needed into a custom 'Sat' typeclass. +-- +-- With @ConstraintKinds@ we can put into code a lot of tools for manipulating +-- these new types without such awkward workarounds. +---------------------------------------------------------------------------- +module Data.Constraint + ( + -- * The Kind of Constraints + Constraint + -- * Dictionary + , Dict(Dict) + -- * Entailment + , (:-)(Sub) + , (\\) + , weaken1, weaken2, contract + , (&&&), (***) + , trans, refl + , top, bottom + -- * Dict is fully faithful + , mapDict + , unmapDict + -- * Reflection + , Class(..) + , (:=>)(..) + ) where +import Control.Monad +#if __GLASGOW_HASKELL__ >= 707 +import Control.Category +#endif +import Control.Applicative +#if __GLASGOW_HASKELL__ < 710 +import Data.Monoid +#endif +import Data.Complex +import Data.Ratio +#if __GLASGOW_HASKELL__ >= 707 +import Data.Data +#endif +import GHC.Prim (Constraint) + +-- | Values of type @'Dict' p@ capture a dictionary for a constraint of type @p@. +-- +-- e.g. +-- +-- @ +-- 'Dict' :: 'Dict' ('Eq' 'Int') +-- @ +-- +-- captures a dictionary that proves we have an: +-- +-- @ +-- instance 'Eq' 'Int +-- @ +-- +-- Pattern matching on the 'Dict' constructor will bring this instance into scope. +-- +data Dict :: Constraint -> * where + Dict :: a => Dict a +#if __GLASGOW_HASKELL__ >= 707 + deriving Typeable + + +instance (Typeable p, p) => Data (Dict p) where + gfoldl _ z Dict = z Dict + toConstr _ = dictConstr + gunfold _ z c = case constrIndex c of + 1 -> z Dict + _ -> error "gunfold" + dataTypeOf _ = dictDataType + +dictConstr :: Constr +dictConstr = mkConstr dictDataType "Dict" [] Prefix + +dictDataType :: DataType +dictDataType = mkDataType "Data.Constraint.Dict" [dictConstr] +#endif + +deriving instance Eq (Dict a) +deriving instance Ord (Dict a) +deriving instance Show (Dict a) + +infixr 9 :- + +-- | This is the type of entailment. +-- +-- @a ':-' b@ is read as @a@ \"entails\" @b@. +-- +-- With this we can actually build a category for 'Constraint' resolution. +-- +-- e.g. +-- +-- Because @'Eq' a@ is a superclass of @'Ord' a@, we can show that @'Ord' a@ +-- entails @'Eq' a@. +-- +-- Because @instance 'Ord' a => 'Ord' [a]@ exists, we can show that @'Ord' a@ +-- entails @'Ord' [a]@ as well. +-- +-- This relationship is captured in the ':-' entailment type here. +-- +-- Since @p ':-' p@ and entailment composes, ':-' forms the arrows of a 'Category' +-- of constraints. However, 'Category' only because sufficiently general to support this +-- instance in GHC 7.8, so prior to 7.8 this instance is unavailable. +-- +-- But due to the coherence of instance resolution in Haskell, this 'Category' +-- has some very interesting properties. Notably, in the absence of +-- @IncoherentInstances@, this category is \"thin\", which is to say that +-- between any two objects (constraints) there is at most one distinguishable +-- arrow. +-- +-- This means that for instance, even though there are two ways to derive +-- @'Ord' a ':-' 'Eq' [a]@, the answers from these two paths _must_ by +-- construction be equal. This is a property that Haskell offers that is +-- pretty much unique in the space of languages with things they call \"type +-- classes\". +-- +-- What are the two ways? +-- +-- Well, we can go from @'Ord' a ':-' 'Eq' a@ via the +-- superclass relationship, and them from @'Eq' a ':-' 'Eq' [a]@ via the +-- instance, or we can go from @'Ord' a ':-' 'Ord' [a]@ via the instance +-- then from @'Ord' [a] ':-' 'Eq' [a]@ through the superclass relationship +-- and this diagram by definition must \"commute\". +-- +-- Diagrammatically, +-- +-- > Ord a +-- > ins / \ cls +-- > v v +-- > Ord [a] Eq a +-- > cls \ / ins +-- > v v +-- > Eq [a] +-- +-- This safety net ensures that pretty much anything you can write with this +-- library is sensible and can't break any assumptions on the behalf of +-- library authors. +newtype a :- b = Sub (a => Dict b) +#if __GLASGOW_HASKELL__ >= 707 + deriving Typeable + +type role (:-) nominal nominal + +-- TODO: _proper_ Data for @(p ':-' q)@ requires @(:-)@ to be cartesian _closed_. +-- +-- This is admissable, but not present by default + +-- constraint should be instance (Typeable p, Typeable q, p |- q) => Data (p :- q) +instance (Typeable p, Typeable q, p, q) => Data (p :- q) where + gfoldl _ z (Sub Dict) = z (Sub Dict) + toConstr _ = subConstr + gunfold _ z c = case constrIndex c of + 1 -> z (Sub Dict) + _ -> error "gunfold" + dataTypeOf _ = subDataType + +subConstr :: Constr +subConstr = mkConstr dictDataType "Sub" [] Prefix + +subDataType :: DataType +subDataType = mkDataType "Data.Constraint.:-" [subConstr] + +-- | Possible since GHC 7.8, when 'Category' was made polykinded. +instance Category (:-) where + id = refl + (.) = trans +#endif + +-- | Assumes 'IncoherentInstances' doesn't exist. +instance Eq (a :- b) where + _ == _ = True + +-- | Assumes 'IncoherentInstances' doesn't exist. +instance Ord (a :- b) where + compare _ _ = EQ + +instance Show (a :- b) where + showsPrec d _ = showParen (d > 10) $ showString "Sub Dict" + +infixl 1 \\ -- required comment + +-- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@ +(\\) :: a => (b => r) -> (a :- b) -> r +r \\ Sub Dict = r + +-------------------------------------------------------------------------------- +-- Constraints form a Category +-------------------------------------------------------------------------------- + +-- | Transitivity of entailment +-- +-- If we view @(':-')@ as a Constraint-indexed category, then this is @('.')@ +trans :: (b :- c) -> (a :- b) -> a :- c +trans f g = Sub $ Dict \\ f \\ g + +-- | Reflexivity of entailment +-- +-- If we view @(':-')@ as a Constraint-indexed category, then this is 'id' +refl :: a :- a +refl = Sub Dict + +-------------------------------------------------------------------------------- +-- (,) is a Bifunctor +-------------------------------------------------------------------------------- + +-- | due to the hack for the kind of @(,)@ in the current version of GHC we can't actually +-- make instances for @(,) :: Constraint -> Constraint -> Constraint@, but @(,)@ is a +-- bifunctor on the category of constraints. This lets us map over both sides. +(***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d) +f *** g = Sub $ Dict \\ f \\ g + +-------------------------------------------------------------------------------- +-- Constraints are Cartesian +-------------------------------------------------------------------------------- + +-- | Weakening a constraint product +-- +-- The category of constraints is Cartesian. We can forget information. +weaken1 :: (a, b) :- a +weaken1 = Sub Dict + +-- | Weakening a constraint product +-- +-- The category of constraints is Cartesian. We can forget information. +weaken2 :: (a, b) :- b +weaken2 = Sub Dict + +-- | Contracting a constraint / diagonal morphism +-- +-- The category of constraints is Cartesian. We can reuse information. +contract :: a :- (a, a) +contract = Sub Dict + +-- | Constraint product +-- +-- > trans weaken1 (f &&& g) = f +-- > trans weaken2 (f &&& g) = g +(&&&) :: (a :- b) -> (a :- c) -> a :- (b, c) +f &&& g = Sub $ Dict \\ f \\ g + +-------------------------------------------------------------------------------- +-- Initial and terminal morphisms +-------------------------------------------------------------------------------- + +-- | Every constraint implies truth +-- +-- These are the terminal arrows of the category, and @()@ is the terminal object. +-- +-- Given any constraint there is a unique entailment of the @()@ constraint from that constraint. +top :: a :- () +top = Sub Dict + +type family Ex (a :: *) (c :: Constraint) :: Constraint +type instance Ex () c = () +type instance Ex Bool c = c + +falso :: (() ~ a) :- Ex a c +falso = Sub Dict + +-- | +-- A bad type coercion lets you derive any constraint you want. +-- +-- These are the initial arrows of the category and @(() ~ Bool)@ is the initial object +-- +-- This demonstrates the law of classical logic +bottom :: (() ~ Bool) :- c +bottom = falso + +-------------------------------------------------------------------------------- +-- Dict is fully faithful +-------------------------------------------------------------------------------- + +-- | Apply an entailment to a dictionary. +-- +-- From a category theoretic perspective 'Dict' is a functor that maps from the category +-- of constraints (with arrows in ':-') to the category Hask of Haskell data types. +mapDict :: (a :- b) -> Dict a -> Dict b +mapDict p Dict = case p of Sub q -> q + +-- | +-- This functor is fully faithful, which is to say that given any function you can write +-- @Dict a -> Dict b@ there also exists an entailment @a :- b@ in the category of constraints +-- that you can build. +unmapDict :: (Dict a -> Dict b) -> a :- b +unmapDict f = Sub (f Dict) + +#if __GLASGOW_HASKELL__ >= 707 +type role Dict nominal +#endif + +-------------------------------------------------------------------------------- +-- Reflection +-------------------------------------------------------------------------------- + +-- | Reify the relationship between a class and its superclass constraints as a class +-- +-- Given a definition such as +-- +-- @ +-- class Foo a => Bar a +-- @ +-- +-- you can capture the relationship between 'Bar a' and its superclass 'Foo a' with +-- +-- @ +-- instance 'Class' (Foo a) (Bar a) where 'cls' = 'Sub' 'Dict' +-- @ +-- +-- Now the user can use 'cls :: Bar a :- Foo a' +class Class b h | h -> b where + cls :: h :- b + +infixr 9 :=> +-- | Reify the relationship between an instance head and its body as a class +-- +-- Given a definition such as +-- +-- @ +-- instance Foo a => Foo [a] +-- @ +-- +-- you can capture the relationship between the instance head and its body with +-- +-- @ +-- instance Foo a ':=>' Foo [a] where 'ins' = 'Sub' 'Dict' +-- @ +class b :=> h | h -> b where + ins :: b :- h + +-- Bootstrapping + +instance Class () (Class b a) where cls = Sub Dict +instance Class () (b :=> a) where cls = Sub Dict + +instance Class b a => () :=> Class b a where ins = Sub Dict +instance (b :=> a) => () :=> b :=> a where ins = Sub Dict + +instance Class () () where cls = Sub Dict +instance () :=> () where ins = Sub Dict + +-- Local, Prelude, Applicative, C.M.I and Data.Monoid instances + +-- Eq +instance Class () (Eq a) where cls = Sub Dict +instance () :=> Eq () where ins = Sub Dict +instance () :=> Eq Int where ins = Sub Dict +instance () :=> Eq Bool where ins = Sub Dict +instance () :=> Eq Integer where ins = Sub Dict +instance () :=> Eq Float where ins = Sub Dict +instance () :=> Eq Double where ins = Sub Dict +instance Eq a :=> Eq [a] where ins = Sub Dict +instance Eq a :=> Eq (Maybe a) where ins = Sub Dict +instance Eq a :=> Eq (Complex a) where ins = Sub Dict +instance Eq a :=> Eq (Ratio a) where ins = Sub Dict +instance (Eq a, Eq b) :=> Eq (a, b) where ins = Sub Dict +instance (Eq a, Eq b) :=> Eq (Either a b) where ins = Sub Dict +instance () :=> Eq (Dict a) where ins = Sub Dict +instance () :=> Eq (a :- b) where ins = Sub Dict + +-- Ord +instance Class (Eq a) (Ord a) where cls = Sub Dict +instance () :=> Ord () where ins = Sub Dict +instance () :=> Ord Bool where ins = Sub Dict +instance () :=> Ord Int where ins = Sub Dict +instance ():=> Ord Integer where ins = Sub Dict +instance () :=> Ord Float where ins = Sub Dict +instance ():=> Ord Double where ins = Sub Dict +instance () :=> Ord Char where ins = Sub Dict +instance Ord a :=> Ord (Maybe a) where ins = Sub Dict +instance Ord a :=> Ord [a] where ins = Sub Dict +instance (Ord a, Ord b) :=> Ord (a, b) where ins = Sub Dict +instance (Ord a, Ord b) :=> Ord (Either a b) where ins = Sub Dict +instance Integral a :=> Ord (Ratio a) where ins = Sub Dict +instance () :=> Ord (Dict a) where ins = Sub Dict +instance () :=> Ord (a :- b) where ins = Sub Dict + +-- Show +instance Class () (Show a) where cls = Sub Dict +instance () :=> Show () where ins = Sub Dict +instance () :=> Show Bool where ins = Sub Dict +instance () :=> Show Ordering where ins = Sub Dict +instance () :=> Show Char where ins = Sub Dict +instance Show a :=> Show (Complex a) where ins = Sub Dict +instance Show a :=> Show [a] where ins = Sub Dict +instance Show a :=> Show (Maybe a) where ins = Sub Dict +instance (Show a, Show b) :=> Show (a, b) where ins = Sub Dict +instance (Show a, Show b) :=> Show (Either a b) where ins = Sub Dict +instance (Integral a, Show a) :=> Show (Ratio a) where ins = Sub Dict +instance () :=> Show (Dict a) where ins = Sub Dict +instance () :=> Show (a :- b) where ins = Sub Dict + +-- Read +instance Class () (Read a) where cls = Sub Dict +instance () :=> Read () where ins = Sub Dict +instance () :=> Read Bool where ins = Sub Dict +instance () :=> Read Ordering where ins = Sub Dict +instance () :=> Read Char where ins = Sub Dict +instance Read a :=> Read (Complex a) where ins = Sub Dict +instance Read a :=> Read [a] where ins = Sub Dict +instance Read a :=> Read (Maybe a) where ins = Sub Dict +instance (Read a, Read b) :=> Read (a, b) where ins = Sub Dict +instance (Read a, Read b) :=> Read (Either a b) where ins = Sub Dict +instance (Integral a, Read a) :=> Read (Ratio a) where ins = Sub Dict + +-- Enum +instance Class () (Enum a) where cls = Sub Dict +instance () :=> Enum () where ins = Sub Dict +instance () :=> Enum Bool where ins = Sub Dict +instance () :=> Enum Ordering where ins = Sub Dict +instance () :=> Enum Char where ins = Sub Dict +instance () :=> Enum Int where ins = Sub Dict +instance () :=> Enum Integer where ins = Sub Dict +instance () :=> Enum Float where ins = Sub Dict +instance () :=> Enum Double where ins = Sub Dict +instance Integral a :=> Enum (Ratio a) where ins = Sub Dict + +-- Bounded +instance Class () (Bounded a) where cls = Sub Dict +instance () :=> Bounded () where ins = Sub Dict +instance () :=> Bounded Ordering where ins = Sub Dict +instance () :=> Bounded Bool where ins = Sub Dict +instance () :=> Bounded Int where ins = Sub Dict +instance () :=> Bounded Char where ins = Sub Dict +instance (Bounded a, Bounded b) :=> Bounded (a,b) where ins = Sub Dict + +-- Num +instance Class () (Num a) where cls = Sub Dict +instance () :=> Num Int where ins = Sub Dict +instance () :=> Num Integer where ins = Sub Dict +instance () :=> Num Float where ins = Sub Dict +instance () :=> Num Double where ins = Sub Dict +instance RealFloat a :=> Num (Complex a) where ins = Sub Dict +instance Integral a :=> Num (Ratio a) where ins = Sub Dict + +-- Real +instance Class (Num a, Ord a) (Real a) where cls = Sub Dict +instance () :=> Real Int where ins = Sub Dict +instance () :=> Real Integer where ins = Sub Dict +instance () :=> Real Float where ins = Sub Dict +instance () :=> Real Double where ins = Sub Dict +instance Integral a :=> Real (Ratio a) where ins = Sub Dict + +-- Integral +instance Class (Real a, Enum a) (Integral a) where cls = Sub Dict +instance () :=> Integral Int where ins = Sub Dict +instance () :=> Integral Integer where ins = Sub Dict + +-- Fractional +instance Class (Num a) (Fractional a) where cls = Sub Dict +instance () :=> Fractional Float where ins = Sub Dict +instance () :=> Fractional Double where ins = Sub Dict +instance RealFloat a :=> Fractional (Complex a) where ins = Sub Dict +instance Integral a :=> Fractional (Ratio a) where ins = Sub Dict + +-- Floating +instance Class (Fractional a) (Floating a) where cls = Sub Dict +instance () :=> Floating Float where ins = Sub Dict +instance () :=> Floating Double where ins = Sub Dict +instance RealFloat a :=> Floating (Complex a) where ins = Sub Dict + +-- RealFrac +instance Class (Real a, Fractional a) (RealFrac a) where cls = Sub Dict +instance () :=> RealFrac Float where ins = Sub Dict +instance () :=> RealFrac Double where ins = Sub Dict +instance Integral a :=> RealFrac (Ratio a) where ins = Sub Dict + +-- RealFloat +instance Class (RealFrac a, Floating a) (RealFloat a) where cls = Sub Dict +instance () :=> RealFloat Float where ins = Sub Dict +instance () :=> RealFloat Double where ins = Sub Dict + +-- Monoid +instance Class () (Monoid a) where cls = Sub Dict +instance () :=> Monoid () where ins = Sub Dict +instance () :=> Monoid Ordering where ins = Sub Dict +instance () :=> Monoid [a] where ins = Sub Dict +instance Monoid a :=> Monoid (Maybe a) where ins = Sub Dict +instance (Monoid a, Monoid b) :=> Monoid (a, b) where ins = Sub Dict + +-- Functor +instance Class () (Functor f) where cls = Sub Dict +instance () :=> Functor [] where ins = Sub Dict +instance () :=> Functor Maybe where ins = Sub Dict +instance () :=> Functor (Either a) where ins = Sub Dict +instance () :=> Functor ((->) a) where ins = Sub Dict +instance () :=> Functor ((,) a) where ins = Sub Dict +instance () :=> Functor IO where ins = Sub Dict +instance Monad m :=> Functor (WrappedMonad m) where ins = Sub Dict + +-- Applicative +instance Class (Functor f) (Applicative f) where cls = Sub Dict +instance () :=> Applicative [] where ins = Sub Dict +instance () :=> Applicative Maybe where ins = Sub Dict +instance () :=> Applicative (Either a) where ins = Sub Dict +instance () :=> Applicative ((->)a) where ins = Sub Dict +instance () :=> Applicative IO where ins = Sub Dict +instance Monoid a :=> Applicative ((,)a) where ins = Sub Dict +instance Monad m :=> Applicative (WrappedMonad m) where ins = Sub Dict + +-- Alternative +instance Class (Applicative f) (Alternative f) where cls = Sub Dict +instance () :=> Alternative [] where ins = Sub Dict +instance () :=> Alternative Maybe where ins = Sub Dict +instance MonadPlus m :=> Alternative (WrappedMonad m) where ins = Sub Dict + +-- Monad +instance Class () (Monad f) where cls = Sub Dict +instance () :=> Monad [] where ins = Sub Dict +instance () :=> Monad ((->) a) where ins = Sub Dict +instance () :=> Monad (Either a) where ins = Sub Dict +instance () :=> Monad IO where ins = Sub Dict + +-- MonadPlus +instance Class (Monad f) (MonadPlus f) where cls = Sub Dict +instance () :=> MonadPlus [] where ins = Sub Dict +instance () :=> MonadPlus Maybe where ins = Sub Dict + +-------------------------------------------------------------------------------- +-- UndecidableInstances +-------------------------------------------------------------------------------- + +instance a :=> Enum (Dict a) where ins = Sub Dict +instance a => Enum (Dict a) where + toEnum _ = Dict + fromEnum Dict = 0 + +instance a :=> Bounded (Dict a) where ins = Sub Dict +instance a => Bounded (Dict a) where + minBound = Dict + maxBound = Dict + +instance a :=> Read (Dict a) where ins = Sub Dict +deriving instance a => Read (Dict a) + +instance a :=> Monoid (Dict a) where ins = Sub Dict +instance a => Monoid (Dict a) where + mappend Dict Dict = Dict + mempty = Dict diff --git a/src/Data/Constraint/Deferrable.hs b/src/Data/Constraint/Deferrable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Constraint/Deferrable.hs @@ -0,0 +1,66 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DeriveDataTypeable #-} + +----------------------------------------------------------------------------- +-- | +-- Module : Data.Constraint.Deferrable +-- Copyright : (C) 2015 Edward Kmett +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Edward Kmett +-- Stability : experimental +-- Portability : non-portable +-- +-- The idea for this trick comes from Dimitrios Vytiniotis. +----------------------------------------------------------------------------- + +module Data.Constraint.Deferrable + ( UnsatisfiedConstraint(..) + , Deferrable(..) + , defer + , deferred + ) where + +import Control.Exception +import Control.Monad +import Data.Constraint +import Data.Proxy +import Data.Typeable (Typeable, cast) + +data UnsatisfiedConstraint = UnsatisfiedConstraint String + deriving (Typeable, Show) + +instance Exception UnsatisfiedConstraint + +-- | Allow an attempt at resolution of a constraint at a later time +class Deferrable (p :: Constraint) where + -- | Resolve a 'Deferrable' constraint with observable failure. + deferEither :: proxy p -> (p => r) -> Either String r + +-- | Defer a constraint for later resolution in a context where we want to upgrade failure into an error +defer :: forall proxy p r. Deferrable p => proxy p -> (p => r) -> r +defer _ r = either (throw . UnsatisfiedConstraint) id $ deferEither (Proxy :: Proxy p) r + +deferred :: forall p. Deferrable p :- p +deferred = Sub $ defer (Proxy :: Proxy p) Dict + +-- We use our own type equality rather than @Data.Type.Equality@ to allow building on GHC 7.6. +data a :~: b where + Refl :: a :~: a + deriving Typeable + +instance (Typeable a, Typeable b) => Deferrable (a ~ b) where + deferEither _ r = case cast (Refl :: a :~: a) :: Maybe (a :~: b) of + Just Refl -> Right r + Nothing -> Left "deferred type equality: type mismatch" + +instance (Deferrable a, Deferrable b) => Deferrable (a, b) where + deferEither _ r = join $ deferEither (Proxy :: Proxy a) $ deferEither (Proxy :: Proxy b) r + +instance (Deferrable a, Deferrable b, Deferrable c) => Deferrable (a, b, c) where + deferEither _ r = join $ deferEither (Proxy :: Proxy a) $ join $ deferEither (Proxy :: Proxy b) $ deferEither (Proxy :: Proxy c) r diff --git a/src/Data/Constraint/Forall.hs b/src/Data/Constraint/Forall.hs new file mode 100644 --- /dev/null +++ b/src/Data/Constraint/Forall.hs @@ -0,0 +1,132 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE PolyKinds #-} +----------------------------------------------------------------------------- +-- | +-- Module : Data.Constraint.Forall +-- Copyright : (C) 2011-2015 Edward Kmett, +-- (C) 2015 Ørjan Johansen, +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Edward Kmett +-- Stability : experimental +-- Portability : non-portable +-- +-- This module uses a trick to provide quantification over constraints. +---------------------------------------------------------------------------- + +module Data.Constraint.Forall + ( Forall, inst + , ForallF, instF + , Forall1, inst1 + , ForallT, instT + ) where + +import Data.Constraint +import Unsafe.Coerce (unsafeCoerce) + +{- The basic trick of this module is to use "skolem" types as test candidates + - for whether a class predicate holds, and if so assume that it holds for all + - types, unsafely coercing the typeclass dictionary. + - + - A previous version of this module used concrete, unexported types as the + - skolems. This turned out to be unsound in the presence of type families. + - There were 3 somewhat distinct issues: + - + - 1. Using closed type families, it is possible to test whether two concrete + - types are equal, even if one of them is not directly importable. + - + - 2. Using just open type families, it is possible to test "at least 2 of + - these n+1 types are equal", thus using the pigeonhole principle to thwart + - any scheme based on having only a finite number of shared skolem types. + - + - 3. Using just pattern matching of types by unification, it is possible + - to extract the skolem types from the application the `Forall p` expands + - to. (Although type families are probably still needed to exploit this.) + - + - András Kovács and Ørjan Johansen independently realized that skolems + - themselves made as type family applications can be used to solve the first + - two problems (and discovered the third problem in the process). As a bonus, + - the resulting code is easy to make polykinded. + - + - Problem 1 is solved by making the type family have no instances, forcing + - GHC to make no assumption about what type a skolem is. + - + - Problem 2 is solved by parametrizing the skolem on the predicate tested + - for. (This is a known trick in predicate logic.) + - + - Problem 3 is solved by making the `Forall p` application expand to a type + - class, and have the *actual* test constraint be a superclass constraint on + - that type class, thus preventing the user directly accessing it. + - + - An unfortunate side effect of the new method is that it tends to trigger + - spurious errors from GHC test for cycles in superclass constraints. András + - Kovács discovered that these can be silenced by yet another use of a type + - family. + - + - David Feuer points out a remaining doubt about the soundness of this scheme: + - GHC *does* know that the skolems created from a single predicate `p` are + - equal. This could in theory apply even if the skolems come from two + - *distinct* invocations of `Forall p`. + - + - However, we don't know any way of bringing two such skolems in contact with + - each other to create an actual exploit. It would seem to require `p` to + - already contain its own skolem, despite there being (hopefully) no way to + - extract it from `Forall p` in order to tie the knot. + -} + +-- the `Skolem*` type families represent skolem variables, do not export! +-- if GHC supports it, these might be made closed with no instances. + +type family Skolem (p :: k -> Constraint) :: k +type family SkolemF (p :: k2 -> Constraint) (f :: k1 -> k2) :: k1 +type family SkolemT1 (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: k1 +type family SkolemT2 (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: k2 + +-- The outer `Forall*` type families prevent GHC from giving a spurious +-- superclass cycle error. +-- The inner `Forall*_` classes prevent the skolem from leaking to the user, +-- which would be disastrous. + +-- | A representation of the quantified constraint @forall a. p a@. +type family Forall (p :: k -> Constraint) :: Constraint where + Forall p = Forall_ p +class p (Skolem p) => Forall_ (p :: k -> Constraint) +instance p (Skolem p) => Forall_ (p :: k -> Constraint) + +-- | A representation of the quantified constraint @forall a. p (f a)@. +type family ForallF (p :: k2 -> Constraint) (f :: k1 -> k2) :: Constraint where + ForallF p f = ForallF_ p f +class p (f (SkolemF p f)) => ForallF_ (p :: k2 -> Constraint) (f :: k1 -> k2) +instance p (f (SkolemF p f)) => ForallF_ (p :: k2 -> Constraint) (f :: k1 -> k2) + +type Forall1 p = Forall p + +-- | A representation of the quantified constraint @forall f a. p (t f a)@. +type family ForallT (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: Constraint where + ForallT p t = ForallT_ p t +class p (t (SkolemT1 p t) (SkolemT2 p t)) => ForallT_ (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) +instance p (t (SkolemT1 p t) (SkolemT2 p t)) => ForallT_ (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) + +-- | Instantiate a quantified @'Forall' p@ constraint at type @a@. +inst :: forall p a. Forall p :- p a +inst = unsafeCoerce (Sub Dict :: Forall p :- p (Skolem p)) + +-- | Instantiate a quantified @'ForallF' p f@ constraint at type @a@. +instF :: forall p f a. ForallF p f :- p (f a) +instF = unsafeCoerce (Sub Dict :: ForallF p f :- p (f (SkolemF p f))) + +-- | Instantiate a quantified constraint on kind @* -> *@. +-- This is now redundant since @'inst'@ became polykinded. +inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall p :- p f +inst1 = inst + +-- | Instantiate a quantified @'ForallT' p t@ constraint at types @f@ and @a@. +instT :: forall (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (f :: k1) (a :: k2). ForallT p t :- p (t f a) +instT = unsafeCoerce (Sub Dict :: ForallT p t :- p (t (SkolemT1 p t) (SkolemT2 p t))) diff --git a/src/Data/Constraint/Lifting.hs b/src/Data/Constraint/Lifting.hs new file mode 100644 --- /dev/null +++ b/src/Data/Constraint/Lifting.hs @@ -0,0 +1,454 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# OPTIONS_GHC -fno-warn-deprecations #-} +module Data.Constraint.Lifting + ( Lifting(..) + , Lifting2(..) + ) where + +import Control.Applicative +import Control.Applicative.Backwards +import Control.Applicative.Lift +import Control.DeepSeq +import Control.Monad +import Control.Monad.Cont.Class +import Control.Monad.Error.Class +import Control.Monad.Fix +import Control.Monad.IO.Class +import Control.Monad.RWS.Class +import Control.Monad.Trans.Cont +import Control.Monad.Trans.Error +import Control.Monad.Trans.Except +import Control.Monad.Trans.Identity +import Control.Monad.Trans.List +import Control.Monad.Trans.Maybe +import Control.Monad.Trans.Reader +import Control.Monad.Trans.RWS.Lazy as Lazy +import Control.Monad.Trans.RWS.Strict as Strict +import Control.Monad.Trans.State.Lazy as Lazy +import Control.Monad.Trans.State.Strict as Strict +import Control.Monad.Trans.Writer.Lazy as Lazy +import Control.Monad.Trans.Writer.Strict as Strict +import Data.Binary +import Data.Complex +import Data.Constraint +#if __GLASGOW_HASKELL__ < 710 +import Data.Foldable +#endif +import Data.Functor.Classes +import Data.Functor.Compose as Functor +import Data.Functor.Identity +import Data.Functor.Product as Functor +import Data.Functor.Reverse as Functor +import Data.Functor.Sum as Functor +import Data.Hashable +#if __GLASGOW_HASKELL__ < 710 +import Data.Monoid +#endif +import Data.Ratio +#if __GLASGOW_HASKELL__ < 710 +import Data.Traversable +#endif +import GHC.Arr + +class Lifting p f where + lifting :: p a :- p (f a) + +instance Lifting Eq [] where lifting = Sub Dict +instance Lifting Ord [] where lifting = Sub Dict +instance Lifting Show [] where lifting = Sub Dict +instance Lifting Read [] where lifting = Sub Dict +instance Lifting Hashable [] where lifting = Sub Dict +instance Lifting Binary [] where lifting = Sub Dict +instance Lifting NFData [] where lifting = Sub Dict + +instance Lifting Eq Maybe where lifting = Sub Dict +instance Lifting Ord Maybe where lifting = Sub Dict +instance Lifting Show Maybe where lifting = Sub Dict +instance Lifting Read Maybe where lifting = Sub Dict +instance Lifting Hashable Maybe where lifting = Sub Dict +instance Lifting Binary Maybe where lifting = Sub Dict +instance Lifting NFData Maybe where lifting = Sub Dict +instance Lifting Monoid Maybe where lifting = Sub Dict + +instance Lifting Eq Ratio where lifting = Sub Dict +-- instance Lifting Show Ratio where lifting = Sub Dict -- requires 7.10 + +instance Lifting Eq Complex where lifting = Sub Dict +instance Lifting Read Complex where lifting = Sub Dict +instance Lifting Show Complex where lifting = Sub Dict + +instance Lifting Monoid ((->) a) where lifting = Sub Dict + +instance Eq a => Lifting Eq (Either a) where lifting = Sub Dict +instance Ord a => Lifting Ord (Either a) where lifting = Sub Dict +instance Show a => Lifting Show (Either a) where lifting = Sub Dict +instance Read a => Lifting Read (Either a) where lifting = Sub Dict +instance Hashable a => Lifting Hashable (Either a) where lifting = Sub Dict +instance Binary a => Lifting Binary (Either a) where lifting = Sub Dict +instance NFData a => Lifting NFData (Either a) where lifting = Sub Dict + +instance Eq a => Lifting Eq ((,) a) where lifting = Sub Dict +instance Ord a => Lifting Ord ((,) a) where lifting = Sub Dict +instance Show a => Lifting Show ((,) a) where lifting = Sub Dict +instance Read a => Lifting Read ((,) a) where lifting = Sub Dict +instance Hashable a => Lifting Hashable ((,) a) where lifting = Sub Dict +instance Binary a => Lifting Binary ((,) a) where lifting = Sub Dict +instance NFData a => Lifting NFData ((,) a) where lifting = Sub Dict +instance Monoid a => Lifting Monoid ((,) a) where lifting = Sub Dict +instance Bounded a => Lifting Bounded ((,) a) where lifting = Sub Dict +instance Ix a => Lifting Ix ((,) a) where lifting = Sub Dict + +instance Functor f => Lifting Functor (Compose f) where lifting = Sub Dict +instance Foldable f => Lifting Foldable (Compose f) where lifting = Sub Dict +instance Traversable f => Lifting Traversable (Compose f) where lifting = Sub Dict +instance Applicative f => Lifting Applicative (Compose f) where lifting = Sub Dict +instance Alternative f => Lifting Alternative (Compose f) where lifting = Sub Dict -- overconstrained +instance (Functor f, Show1 f) => Lifting Show1 (Compose f) where lifting = Sub Dict +instance (Functor f, Eq1 f) => Lifting Eq1 (Compose f) where lifting = Sub Dict +instance (Functor f, Ord1 f) => Lifting Ord1 (Compose f) where lifting = Sub Dict +instance (Functor f, Read1 f) => Lifting Read1 (Compose f) where lifting = Sub Dict +instance (Functor f, Eq1 f, Eq1 g) => Lifting Eq (Compose f g) where lifting = Sub Dict +instance (Functor f, Ord1 f, Ord1 g) => Lifting Ord (Compose f g) where lifting = Sub Dict +instance (Functor f, Read1 f, Read1 g) => Lifting Read (Compose f g) where lifting = Sub Dict +instance (Functor f, Show1 f, Show1 g) => Lifting Show (Compose f g) where lifting = Sub Dict + +instance Functor f => Lifting Functor (Functor.Product f) where lifting = Sub Dict +instance Foldable f => Lifting Foldable (Functor.Product f) where lifting = Sub Dict +instance Traversable f => Lifting Traversable (Functor.Product f) where lifting = Sub Dict +instance Applicative f => Lifting Applicative (Functor.Product f) where lifting = Sub Dict +instance Alternative f => Lifting Alternative (Functor.Product f) where lifting = Sub Dict +instance Monad f => Lifting Monad (Functor.Product f) where lifting = Sub Dict +instance MonadFix f => Lifting MonadFix (Functor.Product f) where lifting = Sub Dict +instance MonadPlus f => Lifting MonadPlus (Functor.Product f) where lifting = Sub Dict +instance Show1 f => Lifting Show1 (Functor.Product f) where lifting = Sub Dict +instance Eq1 f => Lifting Eq1 (Functor.Product f) where lifting = Sub Dict +instance Ord1 f => Lifting Ord1 (Functor.Product f) where lifting = Sub Dict +instance Read1 f => Lifting Read1 (Functor.Product f) where lifting = Sub Dict +instance (Eq1 f, Eq1 g) => Lifting Eq (Functor.Product f g) where lifting = Sub Dict +instance (Ord1 f, Ord1 g) => Lifting Ord (Functor.Product f g) where lifting = Sub Dict +instance (Read1 f, Read1 g) => Lifting Read (Functor.Product f g) where lifting = Sub Dict +instance (Show1 f, Show1 g) => Lifting Show (Functor.Product f g) where lifting = Sub Dict + +instance Functor f => Lifting Functor (Functor.Sum f) where lifting = Sub Dict +instance Foldable f => Lifting Foldable (Functor.Sum f) where lifting = Sub Dict +instance Traversable f => Lifting Traversable (Functor.Sum f) where lifting = Sub Dict +instance Show1 f => Lifting Show1 (Functor.Sum f) where lifting = Sub Dict +instance Eq1 f => Lifting Eq1 (Functor.Sum f) where lifting = Sub Dict +instance Ord1 f => Lifting Ord1 (Functor.Sum f) where lifting = Sub Dict +instance Read1 f => Lifting Read1 (Functor.Sum f) where lifting = Sub Dict +instance (Eq1 f, Eq1 g) => Lifting Eq (Functor.Sum f g) where lifting = Sub Dict +instance (Ord1 f, Ord1 g) => Lifting Ord (Functor.Sum f g) where lifting = Sub Dict +instance (Read1 f, Read1 g) => Lifting Read (Functor.Sum f g) where lifting = Sub Dict +instance (Show1 f, Show1 g) => Lifting Show (Functor.Sum f g) where lifting = Sub Dict + +instance Lifting Functor (Strict.StateT s) where lifting = Sub Dict +instance Lifting Monad (Strict.StateT s) where lifting = Sub Dict +instance Lifting MonadFix (Strict.StateT s) where lifting = Sub Dict +instance Lifting MonadIO (Strict.StateT s) where lifting = Sub Dict +instance Lifting MonadPlus (Strict.StateT s) where lifting = Sub Dict + +instance Lifting Functor (Lazy.StateT s) where lifting = Sub Dict +instance Lifting Monad (Lazy.StateT s) where lifting = Sub Dict +instance Lifting MonadFix (Lazy.StateT s) where lifting = Sub Dict +instance Lifting MonadIO (Lazy.StateT s) where lifting = Sub Dict +instance Lifting MonadPlus (Lazy.StateT s) where lifting = Sub Dict + +instance Lifting Functor (Lazy.RWST r w s) where lifting = Sub Dict +instance Monoid w => Lifting Monad (Lazy.RWST r w s) where lifting = Sub Dict +instance Monoid w => Lifting MonadFix (Lazy.RWST r w s) where lifting = Sub Dict +instance Monoid w => Lifting MonadPlus (Lazy.RWST r w s) where lifting = Sub Dict +instance Monoid w => Lifting MonadIO (Lazy.RWST r w s) where lifting = Sub Dict + +instance Lifting Functor (Strict.RWST r w s) where lifting = Sub Dict +instance Monoid w => Lifting Monad (Strict.RWST r w s) where lifting = Sub Dict +instance Monoid w => Lifting MonadFix (Strict.RWST r w s) where lifting = Sub Dict +instance Monoid w => Lifting MonadPlus (Strict.RWST r w s) where lifting = Sub Dict +instance Monoid w => Lifting MonadIO (Strict.RWST r w s) where lifting = Sub Dict + +instance Lifting Functor (ReaderT e) where lifting = Sub Dict +instance Lifting Applicative (ReaderT e) where lifting = Sub Dict +instance Lifting Alternative (ReaderT e) where lifting = Sub Dict +instance Lifting Monad (ReaderT e) where lifting = Sub Dict +instance Lifting MonadPlus (ReaderT e) where lifting = Sub Dict +instance Lifting MonadFix (ReaderT e) where lifting = Sub Dict +instance Lifting MonadIO (ReaderT e) where lifting = Sub Dict + +instance Lifting Functor (ErrorT e) where lifting = Sub Dict +instance Lifting Foldable (ErrorT e) where lifting = Sub Dict +instance Lifting Traversable (ErrorT e) where lifting = Sub Dict +instance Error e => Lifting Monad (ErrorT e) where lifting = Sub Dict +instance Error e => Lifting MonadFix (ErrorT e) where lifting = Sub Dict +instance Error e => Lifting MonadPlus (ErrorT e) where lifting = Sub Dict -- overconstrained! +instance Error e => Lifting MonadIO (ErrorT e) where lifting = Sub Dict +instance Show e => Lifting Show1 (ErrorT e) where lifting = Sub Dict +instance Eq e => Lifting Eq1 (ErrorT e) where lifting = Sub Dict +instance Ord e => Lifting Ord1 (ErrorT e) where lifting = Sub Dict +instance Read e => Lifting Read1 (ErrorT e) where lifting = Sub Dict +instance (Show e, Show1 m) => Lifting Show (ErrorT e m) where lifting = Sub Dict +instance (Eq e, Eq1 m) => Lifting Eq (ErrorT e m) where lifting = Sub Dict +instance (Ord e, Ord1 m) => Lifting Ord (ErrorT e m) where lifting = Sub Dict +instance (Read e, Read1 m) => Lifting Read (ErrorT e m) where lifting = Sub Dict + +instance Lifting Functor (ExceptT e) where lifting = Sub Dict +instance Lifting Foldable (ExceptT e) where lifting = Sub Dict +instance Lifting Traversable (ExceptT e) where lifting = Sub Dict +instance Lifting Monad (ExceptT e) where lifting = Sub Dict +instance Lifting MonadFix (ExceptT e) where lifting = Sub Dict +instance Monoid e => Lifting MonadPlus (ExceptT e) where lifting = Sub Dict -- overconstrained! +instance Lifting MonadIO (ExceptT e) where lifting = Sub Dict +instance Show e => Lifting Show1 (ExceptT e) where lifting = Sub Dict +instance Eq e => Lifting Eq1 (ExceptT e) where lifting = Sub Dict +instance Ord e => Lifting Ord1 (ExceptT e) where lifting = Sub Dict +instance Read e => Lifting Read1 (ExceptT e) where lifting = Sub Dict +instance (Show e, Show1 m) => Lifting Show (ExceptT e m) where lifting = Sub Dict +instance (Eq e, Eq1 m) => Lifting Eq (ExceptT e m) where lifting = Sub Dict +instance (Ord e, Ord1 m) => Lifting Ord (ExceptT e m) where lifting = Sub Dict +instance (Read e, Read1 m) => Lifting Read (ExceptT e m) where lifting = Sub Dict + +instance Lifting Functor (Strict.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting Applicative (Strict.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting Alternative (Strict.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting Monad (Strict.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting MonadFix (Strict.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting MonadPlus (Strict.WriterT w) where lifting = Sub Dict +instance Lifting Foldable (Strict.WriterT w) where lifting = Sub Dict +instance Lifting Traversable (Strict.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting MonadIO (Strict.WriterT w) where lifting = Sub Dict +instance Show w => Lifting Show1 (Strict.WriterT w) where lifting = Sub Dict +instance Eq w => Lifting Eq1 (Strict.WriterT w) where lifting = Sub Dict +instance Ord w => Lifting Ord1 (Strict.WriterT w) where lifting = Sub Dict +instance Read w => Lifting Read1 (Strict.WriterT w) where lifting = Sub Dict +instance (Show w, Show1 m) => Lifting Show (Strict.WriterT w m) where lifting = Sub Dict +instance (Eq w, Eq1 m) => Lifting Eq (Strict.WriterT w m) where lifting = Sub Dict +instance (Ord w, Ord1 m) => Lifting Ord (Strict.WriterT w m) where lifting = Sub Dict +instance (Read w, Read1 m) => Lifting Read (Strict.WriterT w m) where lifting = Sub Dict + +instance Lifting Functor (Lazy.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting Applicative (Lazy.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting Alternative (Lazy.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting Monad (Lazy.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting MonadFix (Lazy.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting MonadPlus (Lazy.WriterT w) where lifting = Sub Dict +instance Lifting Foldable (Lazy.WriterT w) where lifting = Sub Dict +instance Lifting Traversable (Lazy.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting MonadIO (Lazy.WriterT w) where lifting = Sub Dict +instance Show w => Lifting Show1 (Lazy.WriterT w) where lifting = Sub Dict +instance Eq w => Lifting Eq1 (Lazy.WriterT w) where lifting = Sub Dict +instance Ord w => Lifting Ord1 (Lazy.WriterT w) where lifting = Sub Dict +instance Read w => Lifting Read1 (Lazy.WriterT w) where lifting = Sub Dict +instance (Show w, Show1 m) => Lifting Show (Lazy.WriterT w m) where lifting = Sub Dict +instance (Eq w, Eq1 m) => Lifting Eq (Lazy.WriterT w m) where lifting = Sub Dict +instance (Ord w, Ord1 m) => Lifting Ord (Lazy.WriterT w m) where lifting = Sub Dict +instance (Read w, Read1 m) => Lifting Read (Lazy.WriterT w m) where lifting = Sub Dict + +instance Lifting Functor (ContT r) where lifting = Sub Dict -- overconstrained +instance Lifting Applicative (ContT r) where lifting = Sub Dict -- overconstrained +instance Lifting Monad (ContT r) where lifting = Sub Dict -- overconstrained +instance Lifting MonadIO (ContT r) where lifting = Sub Dict + +instance Lifting Functor IdentityT where lifting = Sub Dict +instance Lifting Applicative IdentityT where lifting = Sub Dict +instance Lifting Alternative IdentityT where lifting = Sub Dict +instance Lifting Monad IdentityT where lifting = Sub Dict +instance Lifting MonadPlus IdentityT where lifting = Sub Dict +instance Lifting MonadFix IdentityT where lifting = Sub Dict +instance Lifting Foldable IdentityT where lifting = Sub Dict +instance Lifting Traversable IdentityT where lifting = Sub Dict +instance Lifting MonadIO IdentityT where lifting = Sub Dict +instance Lifting Show1 IdentityT where lifting = Sub Dict +instance Lifting Read1 IdentityT where lifting = Sub Dict +instance Lifting Ord1 IdentityT where lifting = Sub Dict +instance Lifting Eq1 IdentityT where lifting = Sub Dict +instance Show1 m => Lifting Show (IdentityT m) where lifting = Sub Dict +instance Read1 m => Lifting Read (IdentityT m) where lifting = Sub Dict +instance Ord1 m => Lifting Ord (IdentityT m) where lifting = Sub Dict +instance Eq1 m => Lifting Eq (IdentityT m) where lifting = Sub Dict + +instance Lifting Functor ListT where lifting = Sub Dict +instance Lifting Applicative ListT where lifting = Sub Dict +instance Lifting Alternative ListT where lifting = Sub Dict -- overconstrained +instance Lifting Monad ListT where lifting = Sub Dict +-- instance Lifting MonadFix ListT where lifting = Sub Dict +instance Lifting MonadPlus ListT where lifting = Sub Dict -- overconstrained +instance Lifting Foldable ListT where lifting = Sub Dict +instance Lifting Traversable ListT where lifting = Sub Dict +instance Lifting MonadIO ListT where lifting = Sub Dict +instance Lifting Show1 ListT where lifting = Sub Dict +instance Lifting Read1 ListT where lifting = Sub Dict +instance Lifting Ord1 ListT where lifting = Sub Dict +instance Lifting Eq1 ListT where lifting = Sub Dict +instance Show1 m => Lifting Show (ListT m) where lifting = Sub Dict +instance Read1 m => Lifting Read (ListT m) where lifting = Sub Dict +instance Ord1 m => Lifting Ord (ListT m) where lifting = Sub Dict +instance Eq1 m => Lifting Eq (ListT m) where lifting = Sub Dict + +instance Lifting Functor MaybeT where lifting = Sub Dict +instance Lifting Monad MaybeT where lifting = Sub Dict +-- instance Lifting MonadFix MaybeT where lifting = Sub Dict +instance Lifting MonadPlus MaybeT where lifting = Sub Dict -- overconstrained +instance Lifting Foldable MaybeT where lifting = Sub Dict +instance Lifting Traversable MaybeT where lifting = Sub Dict +instance Lifting MonadIO MaybeT where lifting = Sub Dict +instance Lifting Show1 MaybeT where lifting = Sub Dict +instance Lifting Read1 MaybeT where lifting = Sub Dict +instance Lifting Ord1 MaybeT where lifting = Sub Dict +instance Lifting Eq1 MaybeT where lifting = Sub Dict +instance Show1 m => Lifting Show (MaybeT m) where lifting = Sub Dict +instance Read1 m => Lifting Read (MaybeT m) where lifting = Sub Dict +instance Ord1 m => Lifting Ord (MaybeT m) where lifting = Sub Dict +instance Eq1 m => Lifting Eq (MaybeT m) where lifting = Sub Dict + +instance Lifting Functor Reverse where lifting = Sub Dict +instance Lifting Applicative Reverse where lifting = Sub Dict +instance Lifting Alternative Reverse where lifting = Sub Dict +instance Lifting Foldable Reverse where lifting = Sub Dict +instance Lifting Traversable Reverse where lifting = Sub Dict +instance Lifting Show1 Reverse where lifting = Sub Dict +instance Lifting Read1 Reverse where lifting = Sub Dict +instance Lifting Ord1 Reverse where lifting = Sub Dict +instance Lifting Eq1 Reverse where lifting = Sub Dict +instance Show1 f => Lifting Show (Reverse f) where lifting = Sub Dict +instance Read1 f => Lifting Read (Reverse f) where lifting = Sub Dict +instance Ord1 f => Lifting Ord (Reverse f) where lifting = Sub Dict +instance Eq1 f => Lifting Eq (Reverse f) where lifting = Sub Dict + +instance Lifting Functor Backwards where lifting = Sub Dict +instance Lifting Foldable Backwards where lifting = Sub Dict +instance Lifting Traversable Backwards where lifting = Sub Dict +instance Lifting Applicative Backwards where lifting = Sub Dict +instance Lifting Alternative Backwards where lifting = Sub Dict +instance Lifting Show1 Backwards where lifting = Sub Dict +instance Lifting Read1 Backwards where lifting = Sub Dict +instance Lifting Ord1 Backwards where lifting = Sub Dict +instance Lifting Eq1 Backwards where lifting = Sub Dict +instance Show1 f => Lifting Show (Backwards f) where lifting = Sub Dict +instance Read1 f => Lifting Read (Backwards f) where lifting = Sub Dict +instance Ord1 f => Lifting Ord (Backwards f) where lifting = Sub Dict +instance Eq1 f => Lifting Eq (Backwards f) where lifting = Sub Dict + +instance Lifting Functor Lift where lifting = Sub Dict +instance Lifting Foldable Lift where lifting = Sub Dict +instance Lifting Traversable Lift where lifting = Sub Dict +instance Lifting Applicative Lift where lifting = Sub Dict +instance Lifting Alternative Lift where lifting = Sub Dict +instance Lifting Show1 Lift where lifting = Sub Dict +instance Lifting Read1 Lift where lifting = Sub Dict +instance Lifting Ord1 Lift where lifting = Sub Dict +instance Lifting Eq1 Lift where lifting = Sub Dict +instance Show1 f => Lifting Show (Lift f) where lifting = Sub Dict +instance Read1 f => Lifting Read (Lift f) where lifting = Sub Dict +instance Ord1 f => Lifting Ord (Lift f) where lifting = Sub Dict +instance Eq1 f => Lifting Eq (Lift f) where lifting = Sub Dict + +instance Lifting Eq Identity where lifting = Sub Dict +instance Lifting Ord Identity where lifting = Sub Dict +instance Lifting Show Identity where lifting = Sub Dict +instance Lifting Read Identity where lifting = Sub Dict + +instance Lifting MonadCont MaybeT where lifting = Sub Dict +instance Lifting MonadCont ListT where lifting = Sub Dict +instance Lifting MonadCont IdentityT where lifting = Sub Dict +instance Monoid w => Lifting MonadCont (Strict.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting MonadCont (Lazy.WriterT w) where lifting = Sub Dict +instance Error e => Lifting MonadCont (ErrorT e) where lifting = Sub Dict +instance Lifting MonadCont (ExceptT w) where lifting = Sub Dict +instance Lifting MonadCont (Strict.StateT s) where lifting = Sub Dict +instance Lifting MonadCont (Lazy.StateT s) where lifting = Sub Dict +instance Lifting MonadCont (ReaderT e) where lifting = Sub Dict +instance Monoid w => Lifting MonadCont (Strict.RWST r w s) where lifting = Sub Dict +instance Monoid w => Lifting MonadCont (Lazy.RWST r w s) where lifting = Sub Dict + +instance Lifting (MonadError e) MaybeT where lifting = Sub Dict +instance Lifting (MonadError e) ListT where lifting = Sub Dict +instance Lifting (MonadError e) IdentityT where lifting = Sub Dict +instance Monoid w => Lifting (MonadError e) (Strict.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting (MonadError e) (Lazy.WriterT w) where lifting = Sub Dict +instance Lifting (MonadError e) (Strict.StateT s) where lifting = Sub Dict +instance Lifting (MonadError e) (Lazy.StateT s) where lifting = Sub Dict +instance Lifting (MonadError e) (ReaderT r) where lifting = Sub Dict +instance Monoid w => Lifting (MonadError e) (Strict.RWST r w s) where lifting = Sub Dict +instance Monoid w => Lifting (MonadError e) (Lazy.RWST r w s) where lifting = Sub Dict + +instance Lifting (MonadRWS r w s) MaybeT where lifting = Sub Dict +instance Lifting (MonadRWS r w s) IdentityT where lifting = Sub Dict +instance Error e => Lifting (MonadRWS r w s) (ErrorT e) where lifting = Sub Dict +instance Lifting (MonadRWS r w s) (ExceptT e) where lifting = Sub Dict + +instance Lifting (MonadReader r) MaybeT where lifting = Sub Dict +instance Lifting (MonadReader r) ListT where lifting = Sub Dict +instance Lifting (MonadReader r) IdentityT where lifting = Sub Dict +instance Monoid w => Lifting (MonadReader r) (Strict.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting (MonadReader r) (Lazy.WriterT w) where lifting = Sub Dict +instance Lifting (MonadReader r) (Strict.StateT s) where lifting = Sub Dict +instance Lifting (MonadReader r) (Lazy.StateT s) where lifting = Sub Dict +instance Lifting (MonadReader r) (ExceptT e) where lifting = Sub Dict +instance Error e => Lifting (MonadReader r) (ErrorT e) where lifting = Sub Dict +instance Lifting (MonadReader r) (ContT r') where lifting = Sub Dict + +instance Lifting (MonadState s) MaybeT where lifting = Sub Dict +instance Lifting (MonadState s) ListT where lifting = Sub Dict +instance Lifting (MonadState s) IdentityT where lifting = Sub Dict +instance Monoid w => Lifting (MonadState s) (Strict.WriterT w) where lifting = Sub Dict +instance Monoid w => Lifting (MonadState s) (Lazy.WriterT w) where lifting = Sub Dict +instance Lifting (MonadState s) (ReaderT r) where lifting = Sub Dict +instance Lifting (MonadState s) (ExceptT e) where lifting = Sub Dict +instance Error e => Lifting (MonadState s) (ErrorT e) where lifting = Sub Dict +instance Lifting (MonadState s) (ContT r') where lifting = Sub Dict + +class Lifting2 p f where + lifting2 :: p a :- Lifting p (f a) -- (p a, p b) :- p (f a b) + +instance Lifting2 Eq Either where lifting2 = Sub Dict +instance Lifting2 Ord Either where lifting2 = Sub Dict +instance Lifting2 Show Either where lifting2 = Sub Dict +instance Lifting2 Read Either where lifting2 = Sub Dict +instance Lifting2 Hashable Either where lifting2 = Sub Dict +instance Lifting2 Binary Either where lifting2 = Sub Dict +instance Lifting2 NFData Either where lifting2 = Sub Dict + +instance Lifting2 Eq (,) where lifting2 = Sub Dict +instance Lifting2 Ord (,) where lifting2 = Sub Dict +instance Lifting2 Show (,) where lifting2 = Sub Dict +instance Lifting2 Read (,) where lifting2 = Sub Dict +instance Lifting2 Hashable (,) where lifting2 = Sub Dict +instance Lifting2 Binary (,) where lifting2 = Sub Dict +instance Lifting2 NFData (,) where lifting2 = Sub Dict +instance Lifting2 Monoid (,) where lifting2 = Sub Dict +instance Lifting2 Bounded (,) where lifting2 = Sub Dict +instance Lifting2 Ix (,) where lifting2 = Sub Dict + +instance Lifting2 Functor Compose where lifting2 = Sub Dict +instance Lifting2 Foldable Compose where lifting2 = Sub Dict +instance Lifting2 Traversable Compose where lifting2 = Sub Dict +instance Lifting2 Applicative Compose where lifting2 = Sub Dict +instance Lifting2 Alternative Compose where lifting2 = Sub Dict -- overconstrained + +instance Lifting2 Functor Functor.Product where lifting2 = Sub Dict +instance Lifting2 Foldable Functor.Product where lifting2 = Sub Dict +instance Lifting2 Traversable Functor.Product where lifting2 = Sub Dict +instance Lifting2 Applicative Functor.Product where lifting2 = Sub Dict +instance Lifting2 Alternative Functor.Product where lifting2 = Sub Dict +instance Lifting2 Monad Functor.Product where lifting2 = Sub Dict +instance Lifting2 MonadPlus Functor.Product where lifting2 = Sub Dict +instance Lifting2 MonadFix Functor.Product where lifting2 = Sub Dict +instance Lifting2 Show1 Functor.Product where lifting2 = Sub Dict +instance Lifting2 Eq1 Functor.Product where lifting2 = Sub Dict +instance Lifting2 Ord1 Functor.Product where lifting2 = Sub Dict +instance Lifting2 Read1 Functor.Product where lifting2 = Sub Dict + +instance Lifting2 Functor Functor.Sum where lifting2 = Sub Dict +instance Lifting2 Foldable Functor.Sum where lifting2 = Sub Dict +instance Lifting2 Traversable Functor.Sum where lifting2 = Sub Dict +instance Lifting2 Show1 Functor.Sum where lifting2 = Sub Dict +instance Lifting2 Eq1 Functor.Sum where lifting2 = Sub Dict +instance Lifting2 Ord1 Functor.Sum where lifting2 = Sub Dict +instance Lifting2 Read1 Functor.Sum where lifting2 = Sub Dict diff --git a/src/Data/Constraint/Unsafe.hs b/src/Data/Constraint/Unsafe.hs new file mode 100644 --- /dev/null +++ b/src/Data/Constraint/Unsafe.hs @@ -0,0 +1,65 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE Unsafe #-} +----------------------------------------------------------------------------- +-- | +-- Module : Data.Constraint.Unsafe +-- Copyright : (C) 2011-2015 Edward Kmett +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Edward Kmett +-- Stability : experimental +-- Portability : non-portable +-- +---------------------------------------------------------------------------- +module Data.Constraint.Unsafe + ( Coercible + , unsafeCoerceConstraint + , unsafeDerive + , unsafeUnderive + -- * Sugar + , unsafeApplicative + , unsafeAlternative + ) where + +import Control.Applicative +import Control.Monad +import Data.Constraint +import Unsafe.Coerce + +#if __GLASGOW_HASKELL__ >= 708 + +import Data.Coerce + +#else + +import Control.Newtype + +type Coercible = Newtype + +#endif + +-- | Coerce a dictionary unsafely from one type to another +unsafeCoerceConstraint :: a :- b +unsafeCoerceConstraint = unsafeCoerce refl + +-- | Coerce a dictionary unsafely from one type to a newtype of that type +unsafeDerive :: Coercible n o => (o -> n) -> t o :- t n +unsafeDerive _ = unsafeCoerceConstraint + +-- | Coerce a dictionary unsafely from a newtype of a type to the base type +unsafeUnderive :: Coercible n o => (o -> n) -> t n :- t o +unsafeUnderive _ = unsafeCoerceConstraint + +-- | Construct an Applicative instance from a Monad +unsafeApplicative :: forall m a. Monad m => (Applicative m => m a) -> m a +unsafeApplicative m = m \\ trans (unsafeCoerceConstraint :: Applicative (WrappedMonad m) :- Applicative m) ins + +-- | Construct an Alternative instance from a MonadPlus +unsafeAlternative :: forall m a. MonadPlus m => (Alternative m => m a) -> m a +unsafeAlternative m = m \\ trans (unsafeCoerceConstraint :: Alternative (WrappedMonad m) :- Alternative m) ins