Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WIP: Add quantified constraint superclasses #21

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 0 additions & 45 deletions .github/workflows/haskell-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -62,51 +62,6 @@ jobs:
compilerVersion: 8.6.5
setup-method: hvr-ppa
allow-failure: false
- compiler: ghc-8.4.4
compilerKind: ghc
compilerVersion: 8.4.4
setup-method: hvr-ppa
allow-failure: false
- compiler: ghc-8.2.2
compilerKind: ghc
compilerVersion: 8.2.2
setup-method: hvr-ppa
allow-failure: false
- compiler: ghc-8.0.2
compilerKind: ghc
compilerVersion: 8.0.2
setup-method: hvr-ppa
allow-failure: false
- compiler: ghc-7.10.3
compilerKind: ghc
compilerVersion: 7.10.3
setup-method: hvr-ppa
allow-failure: false
- compiler: ghc-7.8.4
compilerKind: ghc
compilerVersion: 7.8.4
setup-method: hvr-ppa
allow-failure: false
- compiler: ghc-7.6.3
compilerKind: ghc
compilerVersion: 7.6.3
setup-method: hvr-ppa
allow-failure: false
- compiler: ghc-7.4.2
compilerKind: ghc
compilerVersion: 7.4.2
setup-method: hvr-ppa
allow-failure: false
- compiler: ghc-7.2.2
compilerKind: ghc
compilerVersion: 7.2.2
setup-method: hvr-ppa
allow-failure: false
- compiler: ghc-7.0.4
compilerKind: ghc
compilerVersion: 7.0.4
setup-method: hvr-ppa
allow-failure: false
fail-fast: false
steps:
- name: apt
Expand Down
16 changes: 3 additions & 13 deletions some.cabal
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
name: some
version: 1.0.4
x-revision: 1
version: 1.1.0
cabal-version: >=1.10
build-type: Simple
author:
Expand All @@ -25,16 +24,7 @@ description:
If you are unsure which variant to use, use the one in "Data.Some" module.

tested-with:
GHC ==7.0.4
|| ==7.2.2
|| ==7.4.2
|| ==7.6.3
|| ==7.8.4
|| ==7.10.3
|| ==8.0.2
|| ==8.2.2
|| ==8.4.4
|| ==8.6.5
GHC ==8.6.5
|| ==8.8.4
|| ==8.10.4
|| ==9.0.1
Expand Down Expand Up @@ -74,7 +64,7 @@ library

other-modules: Data.GADT.Internal
build-depends:
base >=4.3 && <4.18
base >=4.18 && <4.19
, deepseq >=1.3.0.0 && <1.5

if !impl(ghc >=8.2)
Expand Down
4 changes: 0 additions & 4 deletions src/Data/GADT/Compare.hs
Original file line number Diff line number Diff line change
@@ -1,9 +1,5 @@
{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 704
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
module Data.GADT.Compare (
-- * Equality
GEq (..),
Expand Down
6 changes: 0 additions & 6 deletions src/Data/GADT/DeepSeq.hs
Original file line number Diff line number Diff line change
@@ -1,17 +1,11 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
#if __GLASGOW_HASKELL__ >= 706
{-# LANGUAGE PolyKinds #-}
#endif
#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif
#if (__GLASGOW_HASKELL__ >= 704 && __GLASGOW_HASKELL__ < 707) || __GLASGOW_HASKELL__ >= 801
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
module Data.GADT.DeepSeq (
GNFData (..),
) where
Expand Down
124 changes: 34 additions & 90 deletions src/Data/GADT/Internal.hs
Original file line number Diff line number Diff line change
@@ -1,26 +1,25 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
#if __GLASGOW_HASKELL__ >= 706
{-# LANGUAGE PolyKinds #-}
#endif
#if __GLASGOW_HASKELL__ >= 708
{-# LANGUAGE RoleAnnotations #-}
#endif
#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif
#if __GLASGOW_HASKELL__ >= 800 && __GLASGOW_HASKELL__ < 805
{-# LANGUAGE TypeInType #-}
#endif
#if (__GLASGOW_HASKELL__ >= 704 && __GLASGOW_HASKELL__ < 707) || __GLASGOW_HASKELL__ >= 801
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Safe #-}

-- For GShow
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.GADT.Internal where

import Control.Applicative (Applicative (..))
Expand All @@ -34,9 +33,7 @@ import Data.Type.Equality ((:~:) (..))
import GHC.Generics ((:+:) (..), (:*:) (..))
#endif

#if __GLASGOW_HASKELL__ >=708
import Data.Typeable (Typeable)
#endif

#if MIN_VERSION_base(4,9,0)
#if MIN_VERSION_base(4,10,0)
Expand All @@ -59,6 +56,7 @@ import Data.Kind (Type)
import Data.Kind (Constraint)
#endif

{-# DEPRECATED GShow "Just use the underlying quantified constraint" #-}
-- $setup
-- >>> :set -XKindSignatures -XGADTs -XTypeOperators
-- >>> import Data.Type.Equality
Expand All @@ -69,12 +67,12 @@ import Data.Kind (Constraint)
-- like @(forall a. Show (t a)) => ...@. The easiest way to create instances would probably be
-- to write (or derive) an @instance Show (T a)@, and then simply say:
--
-- > instance GShow t where gshowsPrec = defaultGshowsPrec
#if __GLASGOW_HASKELL__ >= 810
type GShow :: (k -> Type) -> Constraint
#endif
class GShow t where
gshowsPrec :: Int -> t a -> ShowS
-- > instance GShow t
class (forall a. Show (t a)) => GShow t
instance (forall a. Show (t a)) => GShow t

gshowsPrec :: GShow t => Int -> t a -> ShowS
gshowsPrec = showsPrec

-- |If 'f' has a 'Show (f a)' instance, this function makes a suitable default
-- implementation of 'gshowsPrec'.
Expand All @@ -89,59 +87,6 @@ gshows = gshowsPrec (-1)
gshow :: (GShow t) => t a -> String
gshow x = gshows x ""

instance GShow ((:~:) a) where
gshowsPrec _ Refl = showString "Refl"

#if MIN_VERSION_base(4,9,0)
-- | @since 1.0.4
instance GShow ((:~~:) a) where
gshowsPrec _ HRefl = showString "HRefl"
#endif

#if MIN_VERSION_base(4,10,0)
instance GShow TR.TypeRep where
gshowsPrec = showsPrec
#endif

--
-- | >>> gshow (InL Refl :: Sum ((:~:) Int) ((:~:) Bool) Int)
-- "InL Refl"
instance (GShow a, GShow b) => GShow (Sum a b) where
gshowsPrec d = \s -> case s of
InL x -> showParen (d > 10) (showString "InL " . gshowsPrec 11 x)
InR x -> showParen (d > 10) (showString "InR " . gshowsPrec 11 x)

-- | >>> gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)
-- "Pair Refl Refl"
instance (GShow a, GShow b) => GShow (Product a b) where
gshowsPrec d (Pair x y) = showParen (d > 10)
$ showString "Pair "
. gshowsPrec 11 x
. showChar ' '
. gshowsPrec 11 y

#if MIN_VERSION_base(4,6,0)
--
-- | >>> gshow (L1 Refl :: ((:~:) Int :+: (:~:) Bool) Int)
-- "L1 Refl"
--
-- @since 1.0.4
instance (GShow a, GShow b) => GShow (a :+: b) where
gshowsPrec d = \s -> case s of
L1 x -> showParen (d > 10) (showString "L1 " . gshowsPrec 11 x)
R1 x -> showParen (d > 10) (showString "R1 " . gshowsPrec 11 x)

-- | >>> gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)
-- "Refl :*: Refl"
--
-- @since 1.0.4
instance (GShow a, GShow b) => GShow (a :*: b) where
gshowsPrec d (x :*: y) = showParen (d > 6)
$ gshowsPrec 6 x
. showString " :*: "
. gshowsPrec 6 y
#endif

-- |@GReadS t@ is equivalent to @ReadS (forall b. (forall a. t a -> b) -> b)@, which is
-- in turn equivalent to @ReadS (Exists t)@ (with @data Exists t where Exists :: t a -> Exists t@)
#if __GLASGOW_HASKELL__ >= 810
Expand All @@ -164,6 +109,9 @@ type GRead :: (k -> Type) -> Constraint
class GRead t where
greadsPrec :: Int -> GReadS t

-- (forall a. Read (t a)) =>
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Really should be

Suggested change
-- (forall a. Read (t a)) =>
-- (exists a. Read (t a)) =>

GRead ((:~:) a) only reads a :~: a, we're not going to create non-trivial :~: out of nothing. Likewise, in #45 we have

instance forall k1 k2 (a :: k1). k1 ~ k2 => GRead ((:~~:) a :: k2 -> Type)

which is more clearly written (at the cost of less back compat) as

instance forall k1 k2 (a :: k1). k1 ~ k2 => GRead ((:~~:) @k1 @k2 a)

We can only attempt to read when the kinds are the same and there isn't, in fact, any heterogeneity.

-- Skipping because it is rather misleading to use.

greads :: GRead t => GReadS t
greads = greadsPrec (-1)

Expand Down Expand Up @@ -240,7 +188,7 @@ instance (GRead a, GRead b) => GRead (a :+: b) where
#if __GLASGOW_HASKELL__ >= 810
type GEq :: (k -> Type) -> Constraint
#endif
class GEq f where
class (forall a. Eq (f a)) => GEq f where
-- |Produce a witness of type-equality, if one exists.
--
-- A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:
Expand Down Expand Up @@ -357,9 +305,21 @@ data GOrdering a b where
GLT :: GOrdering a b
GEQ :: GOrdering t t
GGT :: GOrdering a b
#if __GLASGOW_HASKELL__ >=708
deriving Typeable
#endif

deriving instance Eq (GOrdering a b)
deriving instance Ord (GOrdering a b)
deriving instance Show (GOrdering a b)

{-
instance Read (GOrdering a b) where
readsPrec _ s = case con of
"GGT" -> [(GGT, rest)]
"GEQ" -> [] -- cannot read without evidence of equality
"GLT" -> [(GLT, rest)]
_ -> []
where (con, rest) = splitAt 3 s
-}

-- |TODO: Think of a better name
--
Expand All @@ -369,20 +329,6 @@ weakenOrdering GLT = LT
weakenOrdering GEQ = EQ
weakenOrdering GGT = GT

instance Eq (GOrdering a b) where
x == y = weakenOrdering x == weakenOrdering y

instance Ord (GOrdering a b) where
compare x y = compare (weakenOrdering x) (weakenOrdering y)

instance Show (GOrdering a b) where
showsPrec _ GGT = showString "GGT"
showsPrec _ GEQ = showString "GEQ"
showsPrec _ GLT = showString "GLT"

instance GShow (GOrdering a) where
gshowsPrec = showsPrec

instance GRead (GOrdering a) where
greadsPrec _ s = case con of
"GGT" -> [(mkSome GGT, rest)]
Expand All @@ -396,7 +342,7 @@ instance GRead (GOrdering a) where
#if __GLASGOW_HASKELL__ >= 810
type GCompare :: (k -> Type) -> Constraint
#endif
class GEq f => GCompare f where
class (GEq f, forall a. Ord (f a)) => GCompare f where
gcompare :: f a -> f b -> GOrdering a b

instance GCompare ((:~:) a) where
Expand Down Expand Up @@ -513,9 +459,7 @@ newtype Some tag = S
withSome :: forall r. (forall a. tag a -> r) -> r
}

#if __GLASGOW_HASKELL__ >= 708
type role Some representational
#endif

-- | Constructor.
mkSome :: tag a -> Some tag
Expand Down
4 changes: 0 additions & 4 deletions src/Data/GADT/Show.hs
Original file line number Diff line number Diff line change
@@ -1,9 +1,5 @@
{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 704
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
module Data.GADT.Show (
-- * Showing
GShow (..),
Expand Down
8 changes: 0 additions & 8 deletions src/Data/Some.hs
Original file line number Diff line number Diff line change
@@ -1,18 +1,10 @@
{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 704
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
-- | An existential type.
--
-- The constructor is exported only on GHC-8 and later.
module Data.Some (
#if __GLASGOW_HASKELL__ >= 801
Some(Some),
#else
Some,
#endif
mkSome,
withSome,
withSomeM,
Expand Down
4 changes: 0 additions & 4 deletions src/Data/Some/Church.hs
Original file line number Diff line number Diff line change
@@ -1,9 +1,5 @@
{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 704
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
module Data.Some.Church (
Some(..),
mkSome,
Expand Down
10 changes: 0 additions & 10 deletions src/Data/Some/GADT.hs
Original file line number Diff line number Diff line change
@@ -1,20 +1,12 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
#if __GLASGOW_HASKELL__ >= 706
{-# LANGUAGE PolyKinds #-}
#endif
#if __GLASGOW_HASKELL__ >= 708
{-# LANGUAGE RoleAnnotations #-}
#endif
#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif
#if __GLASGOW_HASKELL__ >= 704
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif
module Data.Some.GADT (
Some(Some),
mkSome,
Expand Down Expand Up @@ -91,9 +83,7 @@ type Some :: (k -> Type) -> Type
data Some tag where
Some :: tag a -> Some tag

#if __GLASGOW_HASKELL__ >= 708
type role Some representational
#endif

-- | Constructor.
mkSome :: tag a -> Some tag
Expand Down
Loading