diff --git a/Control/Constraint/Combine.hs b/Control/Constraint/Combine.hs new file mode 100644 --- /dev/null +++ b/Control/Constraint/Combine.hs @@ -0,0 +1,36 @@ +{-# LANGUAGE PolyKinds, ConstraintKinds, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-} +{-# OPTIONS_GHC -fno-warn-unused-imports #-} + +-- | This module contains a type-level combinator for combining constraint constructors. +-- +-- This is useful because you can't otherwise write an @'Exists'@ type or @'Existential'@ instance referencing more than one at the same time. +module Control.Constraint.Combine where + +import Data.Exists.Internal -- just for haddock + +-- | Combine two constraint constructors of kind @χ -> 'Constraint'@, where @χ@ is any kind. +-- +-- This is the same as +-- +-- > type (c :&: d) a = (c a, d a) +-- +-- except that it can be partially applied. +-- +-- > f :: ((Eq :&: Enum :&: Bounded) a) => a -> Bool +-- +-- is equivalent to +-- +-- > f :: (Eq a, Enum a, Bounded a) => a -> Bool +class (c a, d a) => (c :&: d) a +instance (c a, d a) => (c :&: d) a +infixl 7 :&: + +-- | The same as @':&:'@. +type c `And` d = c :&: d +infixl 7 `And` + +-- | An empty constraint which implies nothing. +-- +-- @':&:'@ and @'Empty'@ form a type-level monoid with @'Empty'@ as the identity element. +class Empty a +instance Empty a diff --git a/Data/Anything.hs b/Data/Anything.hs new file mode 100644 --- /dev/null +++ b/Data/Anything.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE GADTs, DeriveDataTypeable #-} + +-- | Useless existential datatypes holding evidence of no constraint. +module Data.Anything where + +import Data.Typeable + +-- | A datatype containing anything. You can't do anything with it. +data Anything where + Anything :: a -> Anything + deriving Typeable + +-- | A datatype containing any @* -> *@ kinded type constructor applied to 'a'. You can't do anything with it. +data Anything1 a where + Anything1 :: f a -> Anything1 a + deriving Typeable + +instance Show Anything where + show = const "Anything" + +instance Show (Anything1 a) where + show = const "Anything1" diff --git a/Data/Exists.hs b/Data/Exists.hs new file mode 100644 --- /dev/null +++ b/Data/Exists.hs @@ -0,0 +1,185 @@ +{-# LANGUAGE TypeFamilies, ConstraintKinds, FlexibleInstances, MultiParamTypeClasses #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | Existential datatypes holding evidence of constraints and type classes for existential datatypes. +module Data.Exists (module Data.Exists.Internal) where + +import Data.Exists.Internal +import Data.Exists.Defaults + +import Prelude ((.), error) +import Unsafe.Coerce (unsafeCoerce) +import qualified Data.Traversable as T (foldMapDefault, fmapDefault) +import Data.Dynamic (toDyn, fromDyn) +import Control.Comonad (liftW) +import Control.Constraint.Combine (Empty) +import Data.Typeable (Typeable) +import Control.Exception (Exception) + +import Data.Dynamic (Dynamic) +import GHC.Exts (Any) +import Data.Anything (Anything (..), + Anything1 (..)) +import Control.Exception (SomeException (..)) + +import Prelude (Show (..), + Functor (..)) +import Data.Foldable (Foldable (..)) +import Data.Traversable (Traversable (..)) +import Data.Functor.Contravariant (Contravariant (..)) +import Data.Functor.Extend (Extend (..)) +import Control.Comonad (Comonad (..)) +import Control.Comonad.Env.Class (ComonadEnv (..)) +import Control.Comonad.Traced.Class (ComonadTraced (..)) +import Control.Comonad.Store.Class (ComonadStore (..)) +import Data.Copointed (Copointed (..)) + + +-- | @'ConstraintOf' 'Any' = 'Empty'@ +instance Existential Any where + type ConstraintOf Any = Empty + exists = unsafeCoerce + apply f a = f a + -- this is OK, because f by its type signature must be completely parametric + -- with respect to a + +-- | @'ConstraintOf1' 'Any' = 'Empty'@ +instance Existential1 Any where + type ConstraintOf1 Any = Empty + exists1 = unsafeCoerce + apply1 f a = f a + -- likewise + +-- | @'ConstraintOf' 'Anything' = 'Empty'@ +instance Existential Anything where + type ConstraintOf Anything = Empty + exists = Anything + apply f (Anything a) = f a + +-- | @'ConstraintOf1' 'Anything1' = 'Empty'@ +instance Existential1 Anything1 where + type ConstraintOf1 Anything1 = Empty + exists1 = Anything1 + apply1 f (Anything1 a) = f a + +-- | @'ConstraintOf' 'Dynamic' = 'Typeable'@ +instance Existential Dynamic where + type ConstraintOf Dynamic = Typeable + exists = toDyn + apply f d = f (fromDyn (error "this can't be happening!") d) + -- if I'm thinking correctly, nothing bad can result from this, because: + -- - f can only use what Typeable provides; + -- - typeOf is required to work on bottom values; + -- - if f tries to cast its argument to the type which was in the Dynamic, + -- the argument will be the value from the Dynamic and won't be bottom; + -- - if f tries to cast its argument to a different type, the argument will + -- be bottom, but Typeable won't allow the cast to succeed and it won't + -- matter. + +-- | @'ConstraintOf' 'SomeException' = 'Exception'@ +instance Existential SomeException where + type ConstraintOf SomeException = Exception + exists = SomeException + apply f (SomeException e) = f e + +-- instance Show (Exists Exception) where +-- show = apply show +-- instance Exception (Exists Exception) where +-- fromException = fromExceptionDefault +-- toException = toExceptionDefault +-- +-- this unfortunately can't work, because Exception requires Typeable as a +-- superclass, Typeable only has typeOf as its method, and Typeable.cast will +-- indiscriminately unsafeCoerce based on the result of typeOf: so even if we +-- pass through the typeOf the underlying type, we're screwed because +-- Exists Exception is not physically that type. If we were to use the typeOf +-- (Exists Exception), we'd still be screwed from the other direction, but we +-- can't do that because Typeable isn't available for Constraints. + +instance Show (Exists Show) where + show = showDefault + showsPrec = showsPrecDefault + +instance Functor (Exists1 Functor) where + fmap = fmapDefault + +instance Foldable (Exists1 Foldable) where + fold = foldDefault + foldMap = foldMapDefault + foldl = foldlDefault + foldr = foldrDefault + foldl1 = foldl1Default + foldr1 = foldr1Default + +instance Functor (Exists1 Traversable) where + fmap = T.fmapDefault + +instance Foldable (Exists1 Traversable) where + foldMap = T.foldMapDefault + +instance Traversable (Exists1 Traversable) where + traverse = traverseDefault + sequenceA = sequenceADefault + mapM = mapMDefault + sequence = sequenceDefault + +instance Contravariant (Exists1 Contravariant) where + contramap = contramapDefault + +instance Functor (Exists1 Extend) where + fmap f = apply1 (exists1 . fmap f) + +instance Extend (Exists1 Extend) where + duplicate = duplicateDefault + +instance Functor (Exists1 Comonad) where + fmap = liftW + +instance Extend (Exists1 Comonad) where + duplicate = apply1 (exists1 . fmap exists1 . duplicate) + +instance Comonad (Exists1 Comonad) where + extract = extractDefault + +instance Functor (Exists1 (ComonadEnv e)) where + fmap = liftW + +instance Extend (Exists1 (ComonadEnv e)) where + duplicate = apply1 (exists1 . fmap exists1 . duplicate) + +instance Comonad (Exists1 (ComonadEnv e)) where + extract = apply1 extract + +instance ComonadEnv e (Exists1 (ComonadEnv e)) where + ask = askDefault + +instance Functor (Exists1 (ComonadTraced m)) where + fmap = liftW + +instance Extend (Exists1 (ComonadTraced m)) where + duplicate = apply1 (exists1 . fmap exists1 . duplicate) + +instance Comonad (Exists1 (ComonadTraced m)) where + extract = apply1 extract + +instance ComonadTraced m (Exists1 (ComonadTraced m)) where + trace = traceDefault + +instance Functor (Exists1 (ComonadStore s)) where + fmap = liftW + +instance Extend (Exists1 (ComonadStore s)) where + duplicate = apply1 (exists1 . fmap exists1 . duplicate) + +instance Comonad (Exists1 (ComonadStore s)) where + extract = apply1 extract + +instance ComonadStore s (Exists1 (ComonadStore s)) where + pos = posDefault + peek = peekDefault + peeks = peeksDefault + seek = seekDefault + seeks = seeksDefault + +instance Copointed (Exists1 Copointed) where + copoint = copointDefault diff --git a/Data/Exists/Defaults.hs b/Data/Exists/Defaults.hs new file mode 100644 --- /dev/null +++ b/Data/Exists/Defaults.hs @@ -0,0 +1,135 @@ +{-# LANGUAGE GADTs, TypeFamilies, Rank2Types, ConstraintKinds, FlexibleContexts #-} + +-- | Default functions which can be used as method implementations when writing type class instances for existential datatypes. +module Data.Exists.Defaults where + +import Data.Exists.Internal + +import Prelude (String, Int, ShowS, Monad, (.)) +import Control.Applicative (Applicative) +import Control.Monad (liftM) +import Data.Monoid (Monoid) + +import Prelude (Show (..), + Functor (..)) +import Data.Foldable (Foldable (..)) +import Data.Traversable (Traversable (..)) +import Data.Functor.Contravariant (Contravariant (..)) +import Data.Functor.Extend (Extend (..)) +import Control.Comonad (Comonad (..)) +import Control.Comonad.Env.Class (ComonadEnv (..)) +import Control.Comonad.Traced.Class (ComonadTraced (..)) +import Control.Comonad.Store.Class (ComonadStore (..)) +import Data.Copointed (Copointed (..)) + +-- * Prelude.Show +showDefault :: ExistentialWith Show e => e -> String +showDefault = apply show + +showsPrecDefault :: ExistentialWith Show e => Int -> e -> ShowS +showsPrecDefault n e s = apply (\a -> showsPrec n a s) e + +-- * Prelude.Functor +fmapDefault :: ExistentialWith1 Functor e => (a -> b) -> e a -> e b +fmapDefault f = apply1 (exists1 . fmap f) + +-- * Data.Foldable.Foldable +foldDefault :: (ExistentialWith1 Foldable e, Monoid m) => e m -> m +foldDefault = apply1 fold + +foldMapDefault :: (ExistentialWith1 Foldable e, Monoid m) => (a -> m) -> e a -> m +foldMapDefault f = apply1 (foldMap f) + +foldrDefault :: ExistentialWith1 Foldable e => (a -> b -> b) -> b -> e a -> b +foldrDefault f x = apply1 (foldr f x) + +foldlDefault :: ExistentialWith1 Foldable e => (a -> b -> a) -> a -> e b -> a +foldlDefault f x = apply1 (foldl f x) + +foldr1Default :: ExistentialWith1 Foldable e => (a -> a -> a) -> e a -> a +foldr1Default f = apply1 (foldr1 f) + +foldl1Default :: ExistentialWith1 Foldable e => (a -> a -> a) -> e a -> a +foldl1Default f = apply1 (foldl1 f) + +-- * Data.Traversable.Traversable +traverseDefault :: (ExistentialWith1 Traversable e, Applicative f) => (a -> f b) -> e a -> f (e b) +traverseDefault f = apply1 (fmap exists1 . traverse f) + +sequenceADefault :: (ExistentialWith1 Traversable e, Applicative f) => e (f a) -> f (e a) +sequenceADefault = apply1 (fmap exists1 . sequenceA) + +mapMDefault :: (ExistentialWith1 Traversable e, Monad m) => (a -> m b) -> e a -> m (e b) +mapMDefault f = apply1 (liftM exists1 . mapM f) + +sequenceDefault :: (ExistentialWith1 Traversable e, Monad m) => e (m a) -> m (e a) +sequenceDefault = apply1 (liftM exists1 . sequence) + +-- * Data.Functor.Contravariant.Contravariant +contramapDefault :: ExistentialWith1 Contravariant e => (a -> b) -> e b -> e a +contramapDefault f = apply1 (exists1 . contramap f) + +-- * Data.Functor.Extend.Extend +duplicateDefault :: ExistentialWith1 Extend e => e a -> e (e a) +duplicateDefault = apply1 (exists1 . fmap exists1 . duplicate) + +-- extendDefault :: ExistentialWith1 Extend e => (e a -> b) -> e a -> e b +-- extendDefault = _ + +-- * Control.Comonad.Comonad +extractDefault :: ExistentialWith1 Comonad e => e a -> a +extractDefault = apply1 extract + +-- * Control.Comonad.Env.Class.ComonadEnv +askDefault :: ExistentialWith1 (ComonadEnv env) e => e a -> env +askDefault = apply1 ask + +-- * Control.Comonad.Traced.Class.ComonadTraced +traceDefault :: ExistentialWith1 (ComonadTraced m) e => m -> e a -> a +traceDefault a = apply1 (trace a) + +-- * Control.Comonad.Store.Class.ComonadStore +posDefault :: ExistentialWith1 (ComonadStore s) e => e a -> s +posDefault = apply1 pos + +peekDefault :: ExistentialWith1 (ComonadStore s) e => s -> e a -> a +peekDefault a = apply1 (peek a) + +peeksDefault :: ExistentialWith1 (ComonadStore s) e => (s -> s) -> e a -> a +peeksDefault f = apply1 (peeks f) + +seekDefault :: ExistentialWith1 (ComonadStore s) e => s -> e a -> e a +seekDefault a = apply1 (exists1 . seek a) + +seeksDefault :: ExistentialWith1 (ComonadStore s) e => (s -> s) -> e a -> e a +seeksDefault f = apply1 (exists1 . seeks f) + +-- * Data.Copointed.Copointed +copointDefault :: ExistentialWith1 Copointed e => e a -> a +copointDefault = apply1 copoint + +{-# INLINE showDefault #-} +{-# INLINE showsPrecDefault #-} +{-# INLINE fmapDefault #-} +{-# INLINE foldDefault #-} +{-# INLINE foldMapDefault #-} +{-# INLINE foldrDefault #-} +{-# INLINE foldlDefault #-} +{-# INLINE foldr1Default #-} +{-# INLINE foldl1Default #-} +{-# INLINE traverseDefault #-} +{-# INLINE sequenceADefault #-} +{-# INLINE mapMDefault #-} +{-# INLINE sequenceDefault #-} +{-# INLINE contramapDefault #-} +{-# INLINE duplicateDefault #-} +{- INLINE extendDefault -} +{-# INLINE extractDefault #-} +{-# INLINE askDefault #-} +{-# INLINE traceDefault #-} +{-# INLINE posDefault #-} +{-# INLINE peekDefault #-} +{-# INLINE peeksDefault #-} +{-# INLINE seekDefault #-} +{-# INLINE seeksDefault #-} +{-# INLINE copointDefault #-} diff --git a/Data/Exists/Internal.hs b/Data/Exists/Internal.hs new file mode 100644 --- /dev/null +++ b/Data/Exists/Internal.hs @@ -0,0 +1,100 @@ +{-# LANGUAGE GADTs, TypeFamilies, Rank2Types, ConstraintKinds, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-} + +module Data.Exists.Internal (module Data.Exists.Internal, +-- * The @Constraint@ kind + Constraint) where + +import GHC.Exts (Constraint) + +-- * For kind @*@ + +-- | A datatype which holds a value of a type satisfying the constraint 'c', hiding the type, and evidence for the constraint, so that it can be retrieved by pattern matching later. +-- +-- Example: +-- +-- > foo :: Exists Show +-- > foo = Exists (Just 9 :: Maybe Int) +-- > +-- > printExists :: Exists Show -> IO () +-- > printExists (Exists e) = print e +-- > +-- > main = printExists foo -- prints "Just 9" +data Exists c where + Exists :: c a => a -> Exists c + +-- | A type class to abstract over existential datatypes. +-- +-- Example: +-- +-- > data EShow where +-- > EShow :: Show a => a -> EShow +-- > +-- > instance Existential EShow where +-- > type ConstraintOf EShow = Show +-- > exists = EShow +-- > apply f (EShow a) = f a +-- > +-- > foo :: EShow +-- > foo = exists (Just 9 :: Maybe Int) +-- > +-- > main = apply print foo -- prints "Just 9" +-- +-- Note that had we given 'foo' the type signature +-- +-- > foo :: (Existential e, ConstraintOf e ~ Show) => e +-- +-- GHC would have output an error message, because the instance of @'Existential'@ to use would have been ambiguous. (The @'apply' f '.' 'exists'@ problem is the same as the @'show' '.' 'read'@ problem.) +class Existential e where + type ConstraintOf e :: * -> Constraint + -- | Construct 'e' from a value of a type satisfying the constraint. + exists :: (ConstraintOf e) a => a -> e + -- | Apply a function requiring the constraint to the held value. + apply :: (forall a. (ConstraintOf e) a => a -> r) -> e -> r + +-- | @'ConstraintOf' ('Exists' c) = c@ +instance Existential (Exists c) where + type ConstraintOf (Exists c) = c + exists = Exists + apply f (Exists a) = f a + +-- | An alias for convenience. +-- +-- > foo :: ExistentialWith Show e => e -> IO () +-- +-- is equivalent to +-- +-- > foo :: (Existential e, ConstraintOf e ~ Show) => e -> IO () +class (Existential e, c ~ ConstraintOf e) => ExistentialWith c e +instance (Existential e, c ~ ConstraintOf e) => ExistentialWith c e + +-- | Translate between different existential datatypes holding evidence for the same constraint. +translate :: (ExistentialWith c e1, ExistentialWith c e2) => e1 -> e2 +translate = apply exists + +-- * For kind @* -> *@ + +-- | A @* -> *@ kinded version of @'Exists'@ which holds a value of a type constructor applied to a type, hiding the type constructor, and evidence for a constraint on the type constructor. +data Exists1 c a where + Exists1 :: c f => f a -> Exists1 c a + +-- | A version of @'Existential'@ for kind @* -> *@. +class Existential1 e where + type ConstraintOf1 e :: (* -> *) -> Constraint + -- | Construct 'e' from a value of a type constructor applied to a type where the type constructor satisfies the constraint. + exists1 :: (ConstraintOf1 e) f => f a -> e a + -- | Apply a function requiring the constraint to the held value. + apply1 :: (forall f. (ConstraintOf1 e) f => f a -> r) -> e a -> r + +-- | @'ConstraintOf1' ('Exists1' c) = c@ +instance Existential1 (Exists1 c) where + type ConstraintOf1 (Exists1 c) = c + exists1 = Exists1 + apply1 f (Exists1 a) = f a + +-- | An alias for convenience. A version of 'ExistentialWith' for kind @* -> *@. +class (Existential1 e, c ~ ConstraintOf1 e) => ExistentialWith1 c e +instance (Existential1 e, c ~ ConstraintOf1 e) => ExistentialWith1 c e + +-- | Translate between different existential datatypes holding evidence for the same constraint on a @* -> *@ kinded type constructor. +translate1 :: (ExistentialWith1 c e1, ExistentialWith1 c e2) => e1 a -> e2 a +translate1 = apply1 exists1 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright 2011 Gábor Lehel + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + +3. Neither the name of the author nor the names of his contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR +IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR +ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS +OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) +HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, +STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN +ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/exists.cabal b/exists.cabal new file mode 100644 --- /dev/null +++ b/exists.cabal @@ -0,0 +1,67 @@ +name: exists +category: Constraints +version: 0.1 +author: Gábor Lehel +maintainer: Gábor Lehel +homepage: http://github.com/glehel/exists +copyright: Copyright (C) 2011 Gábor Lehel +license: BSD3 +license-file: LICENSE +stability: experimental +cabal-version: >= 1.10 +build-type: Simple +synopsis: Existential datatypes holding evidence of constraints +description: + This package contains: + . + * Existential datatypes for holding evidence of constraints on types of kind @*@ and @* -> *@; + . + * Type classes for existential datatypes holding evidence of constraints on types of kind @*@ and @* -> *@; + . + * Completely useless existential datatypes holding evidence of no constraint on types of kind @*@ and @* -> *@; + . + * Assorted type class instances for the above; + . + * A type-level combinator for combining constraint constructors. + . + Some of these should maybe be split off into separate packages. + . + "Data.Exists" is the important module, the rest are peripheral. + +source-repository head + type: git + location: git://github.com/glehel/exists.git + +library + default-language: + Haskell2010 + + other-extensions: + GADTs +-- PolyKinds + Rank2Types + TypeFamilies + TypeOperators + ConstraintKinds + FlexibleInstances + UndecidableInstances + MultiParamTypeClasses + + exposed-modules: + Data.Anything + Data.Exists + Data.Exists.Defaults + Control.Constraint.Combine + + other-modules: + Data.Exists.Internal + + build-depends: + base >= 4.5 && < 5, + contravariant == 0.1.*, + comonad == 1.1.*, + comonads-fd == 2.0.*, + pointed == 2.0.* + + ghc-options: + -Wall