Skip to content

Commit

Permalink
WIP: Add quantified constraint superclasses
Browse files Browse the repository at this point in the history
This will not work unless haskell/core-libraries-committee#10 is accepted.
  • Loading branch information
Ericson2314 committed Apr 8, 2022
1 parent 05fc62a commit 18e1b46
Show file tree
Hide file tree
Showing 10 changed files with 35 additions and 168 deletions.
45 changes: 0 additions & 45 deletions .github/workflows/haskell-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -55,51 +55,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
15 changes: 3 additions & 12 deletions some.cabal
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
name: some
version: 1.0.3
version: 1.1.0
x-revision: 2
stability: provisional
cabal-version: >=1.10
Expand All @@ -26,16 +26,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 +65,7 @@ library

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

if !impl(ghc >=7.8)
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,16 +1,10 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
#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
95 changes: 31 additions & 64 deletions src/Data/GADT/Internal.hs
Original file line number Diff line number Diff line change
@@ -1,23 +1,22 @@
{-# 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__ >= 704 && __GLASGOW_HASKELL__ < 707) || __GLASGOW_HASKELL__ >= 801
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Safe #-}
#elif __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Trustworthy #-}
#endif

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

module Data.GADT.Internal where

import Control.Applicative (Applicative (..))
Expand All @@ -28,9 +27,7 @@ import Data.Monoid (Monoid (..))
import Data.Semigroup (Semigroup (..))
import Data.Type.Equality ((:~:) (..))

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

#if MIN_VERSION_base(4,10,0)
import Data.Type.Equality (testEquality)
Expand All @@ -41,6 +38,7 @@ import qualified Type.Reflection as TR
import Data.Kind (Type, Constraint)
#endif

{-# DEPRECATED GShow "Just use the underlying quantified constraint" #-}
-- $setup
-- >>> :set -XKindSignatures -XGADTs

Expand All @@ -49,48 +47,18 @@ import Data.Kind (Type, Constraint)
-- to write (or derive) an @instance Show (T a)@, and then simply say:
--
-- > instance GShow t where gshowsPrec = showsPrec
#if __GLASGOW_HASKELL__ >= 810
type GShow :: (k -> Type) -> Constraint
#endif
class GShow t where
gshowsPrec :: Int -> t a -> ShowS
class (forall a. Show (t a)) => GShow t
instance (forall a. Show (t a)) => GShow t

-- |If 'f' has a 'Show (f a)' instance, this function makes a suitable default
-- implementation of 'gshowsPrec'.
defaultGshowsPrec :: Show (t a) => Int -> t a -> ShowS
defaultGshowsPrec = showsPrec
gshowsPrec :: GShow t => Int -> t a -> ShowS
gshowsPrec = showsPrec

gshows :: GShow t => t a -> ShowS
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,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

-- |@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 @@ -113,6 +81,9 @@ type GRead :: (k -> Type) -> Constraint
class GRead t where
greadsPrec :: Int -> GReadS t

-- (forall a. Read (t a)) =>
-- Skipping because it is rather misleading to use.

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

Expand Down Expand Up @@ -162,7 +133,7 @@ instance (GRead a, GRead b) => GRead (Sum 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 @@ -249,9 +220,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 @@ -261,20 +244,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 @@ -288,7 +257,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 @@ -380,9 +349,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 @@ -90,9 +82,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

0 comments on commit 18e1b46

Please sign in to comment.