**diff options**

author | sjakobi <> | 2019-09-10 12:35:00 (GMT) |
---|---|---|

committer | hdiff <hdiff@hdiff.luite.com> | 2019-09-10 12:35:00 (GMT) |

commit | 01fedd090c668b32f66132018b476e09db1f3701 (patch) | |

tree | 4f31061aa6498699feb6adf22cab10fe2e0a1bd4 | |

parent | 484a2d64edfc3415372d3d7a6e2998c3d8cc7c20 (diff) |

-rw-r--r-- | CHANGELOG.md | 14 | ||||

-rw-r--r-- | Setup.hs | 2 | ||||

-rw-r--r-- | coercible-utils.cabal | 17 | ||||

-rw-r--r-- | src/CoercibleUtils.hs | 200 | ||||

-rw-r--r-- | src/CoercibleUtils/Compose.hs | 51 | ||||

-rw-r--r-- | src/CoercibleUtils/Newtype.hs | 328 | ||||

-rw-r--r-- | test/Spec.hs | 103 |

7 files changed, 517 insertions, 198 deletions

diff --git a/CHANGELOG.md b/CHANGELOG.md index dd2ac91..8fe4913 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,12 +1,24 @@ # Changelog `coercible-utils` uses [PVP Versioning][PVP]. +## [0.1.0] – 2019-09-07 + +* Improve type inference via a new generic `Newtype` class. ([#14], [#16]) +* Improve type signatures to point out which arguments are used only to + direct type inference. ([#13]) + + ## [0.0.0] – 2018-06-29 Initial release. -[Unreleased]: https://github.com/sjakobi/coercible-utils/compare/v0.0.0...HEAD +[Unreleased]: https://github.com/sjakobi/coercible-utils/compare/v0.1.0...HEAD +[0.1.0]: https://github.com/sjakobi/coercible-utils/compare/v0.0.0...v0.1.0 [0.0.0]: https://github.com/sjakobi/coercible-utils/releases/tag/v0.0.0 +[#13]: https://github.com/sjakobi/coercible-utils/pull/13 +[#14]: https://github.com/sjakobi/coercible-utils/pull/14 +[#16]: https://github.com/sjakobi/coercible-utils/pull/16 + [PVP]: https://pvp.haskell.org diff --git a/Setup.hs b/Setup.hs deleted file mode 100644 index 9a994af..0000000 --- a/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/coercible-utils.cabal b/coercible-utils.cabal index 2db934c..086824d 100644 --- a/coercible-utils.cabal +++ b/coercible-utils.cabal @@ -1,29 +1,30 @@ name: coercible-utils -version: 0.0.0 +version: 0.1.0 description: Utility functions for Coercible types. -synopsis: Utility functions for Coercible types. +synopsis: Utility functions for Coercible types homepage: https://github.com/sjakobi/coercible-utils bug-reports: https://github.com/sjakobi/coercible-utils/issues license: BSD3 license-file: LICENSE -author: Simon Jakobi, chessai +author: Simon Jakobi, chessai, David Feuer maintainer: simon.jakobi@gmail.com copyright: 2018 Simon Jakobi, chessai category: Control build-type: Simple extra-doc-files: CHANGELOG.md cabal-version: 1.24 -tested-with: GHC == 7.10.3 - , GHC == 8.0.2 - , GHC == 8.2.2 - , GHC == 8.4.3 +tested-with: GHC == 8.4.4 + , GHC == 8.6.5 + , GHC == 8.8.1 library hs-source-dirs: src exposed-modules: CoercibleUtils + , CoercibleUtils.Compose + , CoercibleUtils.Newtype ghc-options: -Wall - build-depends: base >= 4.8 && < 4.13 + build-depends: base >= 4.11 && < 4.14 default-language: Haskell2010 diff --git a/src/CoercibleUtils.hs b/src/CoercibleUtils.hs index 616ddb3..fa422e7 100644 --- a/src/CoercibleUtils.hs +++ b/src/CoercibleUtils.hs @@ -1,194 +1,22 @@ -{- | -Primarily pulled from the -package @[newtype-generics](http://hackage.haskell.org/package/newtype-generics)@, -and based on Conor McBride's Epigram work, but -generalised to work over anything `Coercible`. - ->>> ala Sum foldMap [1,2,3,4 :: Int] :: Int -10 +{-# language TypeOperators #-} ->>> ala Endo foldMap [(+1), (+2), (subtract 1), (*2) :: Int -> Int] (3 :: Int) :: Int -8 - ->>> under2 Min (<>) 2 (1 :: Int) :: Int -1 +{- | +This module reexports the entire content of the `coercible-utils` package. ->>> over All not (All False) :: All -All {getAll = True) +See the 'CoercibleUtils.Newtype' module for the newtype combinators. -__Note__: All of the functions in this module take an argument that solely +__Note__: Most functions in this package take an argument that solely directs the /type/ of the coercion. The value of this argument is /ignored/. +In each case, this argument has a type that looks like @a \`to\` b@. As the name +of the @to@ type variable suggests, this will typically be a function from +@a@ to @b@. But leaving the type variable completely polymorphic and +unconstrained lets the type signature communicate the fact that the argument +is not used. -} module CoercibleUtils - ( -- * Coercive composition - (#.), (.#) - - -- * The classic "newtype" combinators - , op - , ala, ala' - , under, over - , under2, over2 - , underF, overF + ( module CoercibleUtils.Newtype + , (#.), (.#) ) where -import Data.Coerce (Coercible, coerce) - --- | Coercive left-composition. --- --- >>> (All #. not) True --- All {getAll = False} --- --- The semantics with respect to bottoms are: --- --- @ --- p '#.' ⊥ ≡ ⊥ --- p '#.' f ≡ p '.' f --- @ -infixr 9 #. -(#.) :: Coercible b c => (b -> c) -> (a -> b) -> a -> c -(#.) _ = coerce -{-# INLINE (#.) #-} - --- | Coercive right-composition. --- --- >>> (stimes 2 .# Product) 3 --- Product {getProduct = 9} --- --- The semantics with respect to bottoms are: --- --- @ --- ⊥ '.#' p ≡ ⊥ --- f '.#' p ≡ p '.' f --- @ -infixr 9 .# -(.#) :: Coercible a b => (b -> c) -> (a -> b) -> a -> c -(.#) f _ = coerce f -{-# INLINE (.#) #-} - --- | Reverse the type of a "packer". --- --- >>> op All (All True) --- True --- >>> op (Identity . Sum) (Identity (Sum 3)) --- 3 -op :: Coercible a b - => (a -> b) - -> b - -> a -op = coerce -{-# INLINE op #-} - --- | The workhorse of the package. Given a "packer" and a \"higher order function\" (/hof/), --- it handles the packing and unpacking, and just sends you back a regular old --- function, with the type varying based on the /hof/ you passed. --- --- The reason for the signature of the /hof/ is due to 'ala' not caring about structure. --- To illustrate why this is important, consider this alternative implementation of 'under2': --- --- @ --- under2' :: (Coercible a b, Coercible a' b') --- => (a -> b) -> (b -> b -> b') -> (a -> a -> a') --- under2' pa f o1 o2 = 'ala' pa (\\p -> uncurry f . bimap p p) (o1, o2) --- @ --- --- Being handed the "packer", the /hof/ may apply it in any structure of its choosing – --- in this case a tuple. --- --- >>> ala Sum foldMap [1,2,3,4 :: Int] :: Int --- 10 -ala :: (Coercible a b, Coercible a' b') - => (a -> b) - -> ((a -> b) -> c -> b') - -> c - -> a' -ala pa hof = ala' pa hof id -{-# INLINE ala #-} - --- | The way it differs from the 'ala' function in this package, --- is that it provides an extra hook into the \"packer\" passed to the hof. --- --- However, this normally ends up being 'id', so 'ala' wraps this function and --- passes 'id' as the final parameter by default. --- If you want the convenience of being able to hook right into the /hof/, --- you may use this function. --- --- >>> ala' Sum foldMap length ["hello", "world"] :: Int --- 10 --- --- >>> ala' First foldMap (readMaybe @Int) ["x", "42", "1"] :: Maybe Int --- Just 42 -ala' :: (Coercible a b, Coercible a' b') - => (a -> b) - -> ((d -> b) -> c -> b') - -> (d -> a) - -> c - -> a' -ala' _ hof f = coerce #. hof (coerce f) -{-# INLINE ala' #-} - --- | A very simple operation involving running the function /under/ the "packer". --- --- >>> under Product (stimes 3) (3 :: Int) :: Int --- 27 -under :: (Coercible a b, Coercible a' b') - => (a -> b) - -> (b -> b') - -> a - -> a' -under _ f = coerce f -{-# INLINE under #-} - --- | The opposite of 'under'. I.e., take a function which works on the --- underlying "unpacked" types, and switch it to a function that works --- on the "packer". --- --- >>> over All not (All False) :: All --- All {getAll = True} -over :: (Coercible a b, Coercible a' b') - => (a -> b) - -> (a -> a') - -> b - -> b' -over _ f = coerce f -{-# INLINE over #-} - --- | Lower a binary function to operate on the underlying values. --- --- >>> under2 Any (<>) True False :: Bool --- True -under2 :: (Coercible a b, Coercible a' b') - => (a -> b) - -> (b -> b -> b') - -> a - -> a - -> a' -under2 _ f = coerce f -{-# INLINE under2 #-} - --- | The opposite of 'under2'. -over2 :: (Coercible a b, Coercible a' b') - => (a -> b) - -> (a -> a -> a') - -> b - -> b - -> b' -over2 _ f = coerce f -{-# INLINE over2 #-} - --- | 'under' lifted into a 'Functor'. -underF :: (Coercible a b, Coercible a' b', Functor f, Functor g) - => (a -> b) - -> (f b -> g b') - -> f a - -> g a' -underF _ f = fmap coerce . f . fmap coerce -{-# INLINE underF #-} - --- | 'over' lifted into a 'Functor'. -overF :: (Coercible a b, Coercible a' b', Functor f, Functor g) - => (a -> b) - -> (f a -> g a') - -> f b - -> g b' -overF _ f = fmap coerce . f . fmap coerce -{-# INLINE overF #-} +import CoercibleUtils.Compose ((#.), (.#)) +import CoercibleUtils.Newtype diff --git a/src/CoercibleUtils/Compose.hs b/src/CoercibleUtils/Compose.hs new file mode 100644 index 0000000..e6c205c --- /dev/null +++ b/src/CoercibleUtils/Compose.hs @@ -0,0 +1,51 @@ +{-# language TypeOperators #-} + +{-| +Coercive function composition. + +__Note__: The functions in this module take an argument that solely +directs the /type/ of the coercion. The value of this argument is /ignored/. +In each case, this argument has a type that looks like @a \`to\` b@. As the name +of the @to@ type variable suggests, this will typically be a function from +@a@ to @b@. But leaving the type variable completely polymorphic and +unconstrained lets the type signature communicate the fact that the argument +is not used. +-} +module CoercibleUtils.Compose + ( (#.) + , (.#) + ) where + +import Data.Coerce (Coercible, coerce) + +-- | Coercive left-composition. +-- +-- >>> (All #. not) True +-- All {getAll = False} +-- +-- The semantics with respect to bottoms are: +-- +-- @ +-- p '#.' ⊥ ≡ ⊥ +-- p '#.' f ≡ p '.' f +-- @ +infixr 9 #. +(#.) :: Coercible b c => (b `to` c) -> (a -> b) -> a -> c +(#.) _ = coerce +{-# INLINE (#.) #-} + +-- | Coercive right-composition. +-- +-- >>> (stimes 2 .# Product) 3 +-- Product {getProduct = 9} +-- +-- The semantics with respect to bottoms are: +-- +-- @ +-- ⊥ '.#' p ≡ ⊥ +-- f '.#' p ≡ p '.' f +-- @ +infixr 9 .# +(.#) :: Coercible a b => (b -> c) -> (a `to` b) -> a -> c +(.#) f _ = coerce f +{-# INLINE (.#) #-} diff --git a/src/CoercibleUtils/Newtype.hs b/src/CoercibleUtils/Newtype.hs new file mode 100644 index 0000000..ee2e1f7 --- /dev/null +++ b/src/CoercibleUtils/Newtype.hs @@ -0,0 +1,328 @@ +{-# language FlexibleContexts #-} +{-# language FlexibleInstances #-} +{-# language MultiParamTypeClasses #-} +{-# language ScopedTypeVariables #-} +{-# language TypeFamilies #-} +{-# language TypeOperators #-} +{-# language DataKinds #-} +{-# language UndecidableInstances #-} +{-# language ConstraintKinds #-} +{-# language PolyKinds #-} + +{- | +A version of the 'Newtype' typeclass and related functions. The API is +primarily pulled from Conor McBride's Epigram work. The general idea is that we +can manipulate types in terms of newtypes around them or newtypes in terms of +their underlying types. Some examples: + +>>> ala Sum foldMap [1,2,3,4] +10 + +>>> ala Endo foldMap [(+1), (+2), (subtract 1), (*2)] 3 +8 + +>>> under2 Min (<>) 2 1 +1 + +>>> over All not (All False) +All {getAll = True) + +The version of the 'Newtype' class exported by this module has an instance for +*all* and *only* newtypes with 'Generic' instances whose generated +'Coercible' instances are visible. Users need not, and probably should not, write +their own instances. + +Like McBride's version, and unlike the one in @newtype-generics@, this version +has two parameters: one for the newtype and one for the underlying type. This +is mostly a matter of taste. + +__Note__: Most functions in this module take an argument representing a newtype +constructor. This is used only for its type. To make that clear, the type of +that argument is allowed to be extremely polymorphic: @o \`to\` n@ rather than +@o -> n@. Unfortunately, GHCi displays this as @to o n@, which is ugly but +equivalent. + +General approach: When the type variables @n@ and @o@ appear, @n@ is required +to be a newtype wrapper around @o@. Similarly, when the type variables @n'@ and +@o'@ appear as well, @n'@ is required to be a newtype wrapper around @o'@. +Furthermore, in this case, @n@ and @n'@ are required to be the /same newtype/, +with possibly different type arguments. See 'Similar' for detailed +documentation. + +@since TODO +-} +module CoercibleUtils.Newtype + ( Newtype + , IsNewtype + , HasUnderlying + , O + , Similar + , pack + , unpack + , op + , ala + , ala' + , under + , over + , under2 + , over2 + , underF + , overF + ) where + +import GHC.Generics +import Data.Coerce +import GHC.TypeLits (TypeError, ErrorMessage (..)) +import CoercibleUtils.Compose ((#.), (.#)) +import Data.Kind (Constraint) + +-- | Get the underlying type of a newtype. +-- +-- @ +-- data N = N Int deriving Generic +-- -- O N = Int +-- @ +type O x = GO (Rep x) + +-- | Get the underlying type of a newtype from its generic +-- representation. +type family GO rep where + GO (D1 _d (C1 _c (S1 _s (K1 _i a)))) = a + +-- | Given types @x@ and @o@, produce a constraint requiring that @x@ be a +-- newtype whose underlying type is @o@. +type NewtypeF x o = GNewtypeF x (Rep x) o + +-- | Putting a newtype check and 'TypeError' call in 'GO' and then requiring @o +-- ~ O n@ doesn't get us a custom type error when we want one. Calculating the +-- constraint with an error case, however, seems to do the trick. +type family GNewtypeF x rep o :: Constraint where + GNewtypeF _x (D1 ('MetaData _n _m _p 'True) (C1 _c (S1 _s (K1 _i a)))) o = a ~ o + GNewtypeF x _rep _o = TypeError + ('Text "There is no " ':<>: 'ShowType Newtype ':<>: 'Text " instance for" + ':$$: 'Text " " ':<>: 'ShowType x + ':$$: 'Text "because it is not a newtype.") + +-- | @Newtype n o@ means that @n@ is a newtype wrapper around @o@. @n@ must be +-- an instance of 'Generic'. Furthermore, the @'Coercible' n o@ instance must +-- be visible; this typically means the newtype constructor is visible, but the +-- instance could also have been brought into view by pattern matching on a +-- 'Data.Type.Coercion.Coercion'. +class Coercible n o => Newtype (n :: k) (o :: k) + +-- The Generic n constraint gives a much better type error if n is not an +-- instance of Generic. Without that, there's just a mysterious message +-- involving GO and Rep. With it, the lousy error message still shows up, but +-- at least there's also a good one. +instance (Generic n, NewtypeF n o, Coercible n o) => Newtype n o + +-- | A single-parameter version of 'Newtype', similar to the @Newtype@ class in +-- @newtype-generics@. +-- +-- @Newtype n o@ is equivalent to @(IsNewtype n, o ~ O n)@. +class Newtype n (O n) => IsNewtype n +instance Newtype n (O n) => IsNewtype n + +-- | A version of 'Newtype' with the parameters flipped, for partial +-- application. +class Newtype n o => HasUnderlying o n +instance Newtype n o => HasUnderlying o n + +-- | Two types are @Similar@ if they are built from +-- the same type constructor and the same kind arguments. +-- +-- @Sum Int@ and @Sum Bool@ are @Similar@. +-- +-- @Sum Int@ and @Product Int@ are not @Similar@ +-- because they are built from different type constructors. +-- +-- @Const Int Char@ and @Const Int Maybe@ are not @Similar@ +-- because they have different kind arguments. +class Similar (n :: k) (n' :: k) +-- See [Note: Similar implementation] + +instance (Similar' n n', Similar' n' n) => Similar n n' + +-- | Given a type of the form (f b), try to extract b, assuming that b is of +-- kind kb. Note that kb itself is an implicit argument to GetArg; the +-- surrounding context of the call must determine kb. +type family GetArg (x :: kx) :: kb where + GetArg (_ b) = b + +-- | Given a type of the form (f b), try to extract f, assuming that f is of +-- kind kf. Note that kf itself is an implicit argument to GetFun; the +-- surrounding context of the call must determine kf. +type family GetFun (x :: kx) :: kf where + GetFun (f _) = f + +-- | Given types @n@ and @n'@, produce a constraint requiring that @n'@ be +-- built from the same newtype constructor as @n@. See [Note: Similar +-- implementation]. +type family Similar' (n :: k) (n' :: k) :: Constraint where + Similar' (f (_a :: ka)) n' = + ( Similar' f (GetFun n') + , n' ~ GetFun n' (GetArg n' :: ka)) + Similar' f g = f ~ g +-- We capture the kind of the argument as ka, and pass it to GetArg. +-- The kind of the first call to GetFun is fixed by the kind of f, +-- while the kind of the second is fixed by the kind of n' and the +-- imposed kind, ka, of GetArg. + +{- +[Note: Similar implementation] + +The Similar class is what really separates this implementation of this API from +all previous ones of which I am aware. Since it's not the simplest thing, I'll +give an extended description of the implementation here. + +We really want n to give us information about n'. It's also nice (for typed +holes and error messages, particularly) if n' gives us information about n. +Since we may know nothing, a priori, about one of those, we have to be a bit +careful not to force a match on one when the other is the one with information. +The horrible way to do that (even worse :t results!) is with INCOHERENT +typeclass instances. Ignoring that awfulness, the thing to do is to require n' +to have a structure calculated from n and the other way around, "in parallel". +Similar' n n' matches on n, producing a constraint. Suppose we have n ~ F a b. +Then we get + + Similar' (F a b) n' + (Similar' (F a) (GetFun n'), n' ~ GetFun n' (GetArg n')) + +We have now constrained things only a little: n' is required to have the form p +q for some p and q, where F a and p have the same kind and b and q have the +same kind. Substituting in p and q, we continue: + + (Similar' (F a) p, n' ~ p q) + ((Similar' F (GetFun p), p ~ GetFun p (GetArg p)), n' ~ p q) + +Let's set r ~ GetFun p and s ~ GetArg p. Then + + ((Similar' F r, p ~ r s), n' ~ p q) + +We've now reached the base case! Yay! So the last step is + + ((F ~ r, p ~ r s), n' ~ p q) + +which then simplifies to + + n' ~ F s q + +Undoing the substitutions we made, + + n' ~ F (GetArg (GetFun n')) (GetArg n') + +The arguments in that constraint are completely useless (as far as I know), but +we need to put it all together like that to get what we're after: an equality +constraint on n' itself that lets GHC know it's F x y for some x and y to be +determined. Very often, those are then fixed by the type o' and the Newtype n' +o' constraint, which at first seems backwards. Say we consider Sum. We have + + type Rep (Sum a) = M1 _ _ (M1 _ _ (M1 _ _ (K1 _ a))) + +This can reduce as soon as GHC sees we have Sum whatever! So then the +NewtypeF-calculated constraint can constrain the type argument to whatever's +required to wrap the new contents. Magic! +-} + +-- | Wrap a value with a newtype constructor. +pack :: Newtype n o => o -> n +pack = coerce + +-- | Unwrap a newtype constructor from a value. +unpack :: Newtype n o => n -> o +unpack = coerce + +-- | Reverse the type of a "packer". +-- +-- >>> op All (All True) +-- True +-- >>> op (Identity . Sum) (Identity (Sum 3)) +-- 3 +op :: Coercible a b + => (a `to` b) + -> b + -> a +op _ = coerce +{-# INLINE op #-} + +-- | The workhorse of the package. Given a "packer" and a \"higher order function\" (/hof/), +-- it handles the packing and unpacking, and just sends you back a regular old +-- function, with the type varying based on the /hof/ you passed. +-- +-- The reason for the signature of the /hof/ is due to 'ala' not caring about structure. +-- To illustrate why this is important, consider this alternative implementation of 'under2': +-- +-- > under2 :: (Newtype n o, Newtype n' o') +-- > => (o -> n) -> (n -> n -> n') -> (o -> o -> o') +-- > under2' pa f o0 o1 = ala pa (\p -> uncurry f . bimap p p) (o0, o1) +-- +-- Being handed the "packer", the /hof/ may apply it in any structure of its choosing – +-- in this case a tuple. +-- +-- >>> ala Sum foldMap [1,2,3,4] +-- 10 +ala :: (Newtype n o, Newtype n' o', Similar n n') + => (o `to` n) -> ((o -> n) -> b -> n') -> (b -> o') +ala pa hof = ala' pa hof id + +-- | This is the original function seen in Conor McBride's work. +-- The way it differs from the 'ala' function in this package, +-- is that it provides an extra hook into the \"packer\" passed to the hof. +-- However, this normally ends up being @id@, so 'ala' wraps this function and +-- passes @id@ as the final parameter by default. +-- If you want the convenience of being able to hook right into the hof, +-- you may use this function. +-- +-- >>> ala' Sum foldMap length ["hello", "world"] +-- 10 +-- +-- >>> ala' First foldMap (readMaybe @Int) ["x", "42", "1"] +-- Just 42 +ala' :: (Newtype n o, Newtype n' o', Similar n n') + => (o `to` n) -> ((a -> n) -> b -> n') -> (a -> o) -> (b -> o') +--ala' _ hof f = unpack . hof (coerce . f) +ala' _ = coerce + +-- | A very simple operation involving running the function \'under\' the newtype. +-- +-- >>> under Product (stimes 3) 3 +-- 27 +under :: (Newtype n o, Newtype n' o', Similar n n') + => (o `to` n) -> (n -> n') -> (o -> o') +under _ f = unpack #. f .# coerce + +-- | The opposite of 'under'. I.e., take a function which works on the +-- underlying types, and switch it to a function that works on the newtypes. +-- +-- >>> over All not (All False) +-- All {getAll = True} +over :: (Newtype n o, Newtype n' o', Similar n n') + => (o `to` n) -> (o -> o') -> (n -> n') +over _ f = pack #. f .# coerce + +-- | Lower a binary function to operate on the underlying values. +-- +-- >>> under2 Any (<>) True False +-- True +under2 :: (Newtype n o, Newtype n' o', Similar n n') + => (o `to` n) -> (n -> n -> n') -> (o -> o -> o') +--under2 _ f o0 o1 = unpack $ f (coerce o0) (coerce o1) +under2 _ = coerce + +-- | The opposite of 'under2'. +over2 :: (Newtype n o, Newtype n' o', Similar n n') + => (o `to` n) -> (o -> o -> o') -> (n -> n -> n') +--over2 _ f n0 n1 = pack $ f (coerce n0) (coerce n1) +over2 _ = coerce + +-- | 'under' lifted into a functor. +underF :: ( Newtype n o, Coercible (f o) (f n) + , Coercible (g n') (g o'), Newtype n' o', Similar n n') + => (o `to` n) -> (f n -> g n') -> (f o -> g o') +underF _ f = coerce #. f .# coerce + +-- | 'over' lifted into a functor. +overF :: ( Newtype n o, Coercible (f n) (f o), Coercible (g o') (g n') + , Newtype n' o', Similar n n') + => (o `to` n) -> (f o -> g o') -> (f n -> g n') +overF _ f = coerce #. f .# coerce diff --git a/test/Spec.hs b/test/Spec.hs index 04ed3df..9d2ed06 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -1,3 +1,104 @@ +{-# language PartialTypeSignatures #-} +-- We definitely don't want to infer the types of the test functions +-- based on how they're *used*; if their implementations and (partial) +-- signatures aren't sufficient, then we don't want them to have +-- Typeable instances. +{-# language NoMonomorphismRestriction #-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} + +module Main (main) where +import Data.Monoid (Sum (..), All (..)) +import CoercibleUtils.Newtype +import Type.Reflection + +-- We don't want defaults making it look like things are working +-- if they're not! +default () + +pack_test0 :: _ -> All +pack_test0 = pack + +pack_test1a :: _ -> Sum Int +pack_test1a = pack + +pack_test1b :: Int -> Sum _ +pack_test1b = pack + +unpack_test0 :: All -> _ +unpack_test0 = unpack + +unpack_test1a :: Sum Int -> _ +unpack_test1a = unpack + +unpack_test1b :: Sum _ -> Int +unpack_test1b = unpack + +-- Fix n +ala_test0a + :: (_ -> All) -> (_ -> Bool -> _) -> Bool -> _ +ala_test0a = ala + +-- Fix n' +ala_test0b + :: (_ -> _) -> (_ -> Bool -> All) -> (Bool -> _) +ala_test0b = ala + +-- Fix o and o', partially fix n +ala_test1a :: (Integer -> Sum _) -> (_ -> [Integer] -> _) -> [Integer] -> Word +ala_test1a = ala + -- => (o `to` n) -> ((o -> n) -> b -> n') -> (b -> o') + +-- Fix o', partially fix n, and partially fix n' +ala_test1b :: (_ -> Sum _) -> ((_ -> _ Integer) -> [Integer] -> _) -> [Integer] -> Word +ala_test1b = ala + +-- Fix o and n'; infer o' and n +ala_test1c :: (Integer -> _) -> ((_ -> _) -> [Integer] -> Sum Word) -> [Integer] -> _ +ala_test1c = ala + +-- Fix o' and n; infer o and n' +ala_test1d :: (_ -> Sum Integer) -> (_ -> [Integer] -> _) -> [Integer] -> Word +ala_test1d = ala + +under_test0a :: (_ -> All) -> _ -> _ -> _ +under_test0a = under + +under_test0b :: (_ -> _) -> (_ -> All) -> _ -> _ +under_test0b = under + +over_test0a :: (_ -> All) -> _ -> _ -> _ +over_test0a = over + +over_test0b :: (_ -> _) -> _ -> _ -> All +over_test0b = over + main :: IO () -main = putStrLn ("Test suite not yet implemented" :: String) +main = do + print $ (pack True :: All) + print $ unpack (All True) + print $ ala Sum foldMap [1..10 :: Int] + print $ under Sum (fmap (+1)) (3 :: Int) + print $ over Sum (+3) (Sum (3 :: Int)) + + -- Make sure the types are monomorphic. This is guaranteed by the + -- fact that the Typeable instances are resolved. Also make sure these + -- functions have the expected types! + print $ typeOf pack_test0 + print $ typeOf pack_test1a + print $ typeOf pack_test1b + print $ typeOf unpack_test0 + print $ typeOf unpack_test1a + print $ typeOf unpack_test1b + + print $ typeOf ala_test0a + print $ typeOf ala_test0b + print $ typeOf ala_test1a + print $ typeOf ala_test1b + print $ typeOf ala_test1c + print $ typeOf ala_test1d + + print $ typeOf under_test0a + print $ typeOf under_test0b + print $ typeOf over_test0a + print $ typeOf over_test0b |