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 Oct 1, 2022
1 parent ca50b27 commit 0b40a5b
Show file tree
Hide file tree
Showing 10 changed files with 38 additions and 195 deletions.
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)) =>
-- 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

0 comments on commit 0b40a5b

Please sign in to comment.