diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,14 @@ +# Version 0.5 + +* BREAKING: Depend on `singletons == 2.3.*`. + +* Add `same{1,2,3,4}`. + +* Add dependencies on `cborg` and `serialise` + +* Add instances for `serialise` (binary CBOR encoding/decoding) + + # Version 0.4 * BREAKING: Decouple `binary` and `cereal` instances from `bytes`. This diff --git a/LICENSE.txt b/LICENSE.txt --- a/LICENSE.txt +++ b/LICENSE.txt @@ -1,4 +1,4 @@ -Copyright (c) 2015-2017, Renzo Carbonara +Copyright (c) 2015-2018, Renzo Carbonara All rights reserved. diff --git a/exinst.cabal b/exinst.cabal --- a/exinst.cabal +++ b/exinst.cabal @@ -1,21 +1,21 @@ name: exinst -version: 0.4 +version: 0.5 author: Renzo Carbonara maintainer: renzoλcarbonara.com.ar -copyright: Renzo Carbonara 2015-2017 +copyright: Renzo Carbonara 2015-2018 license: BSD3 license-file: LICENSE.txt extra-source-files: README.md CHANGELOG.md category: Data build-type: Simple cabal-version: >=1.18 -synopsis: Recover type indexes and instances for your existentialized types. +synopsis: Dependent pairs and their instances. homepage: https://github.com/k0001/exinst bug-reports: https://github.com/k0001/exinst/issues library - hs-source-dirs: src/lib + hs-source-dirs: lib default-language: Haskell2010 exposed-modules: Exinst @@ -28,37 +28,47 @@ base >=4.9 && <5.0 , constraints >=0.4 , profunctors >=5.0 - , singletons >=2.2 + , singletons >=2.3.1 ghcjs-options: -Wall -O3 ghc-options: -Wall -O2 if flag(aeson) build-depends: aeson other-modules: Exinst.Instances.Aeson + cpp-options: -DHAS_aeson if flag(binary) || flag(bytes) build-depends: binary other-modules: Exinst.Instances.Binary + cpp-options: -DHAS_binary if flag(bytes) build-depends: bytes >=0.15 other-modules: Exinst.Instances.Bytes + cpp-options: -DHAS_bytes if flag(cereal) || flag(bytes) build-depends: cereal other-modules: Exinst.Instances.Cereal + cpp-options: -DHAS_cereal if flag(deepseq) build-depends: deepseq other-modules: Exinst.Instances.DeepSeq + cpp-options: -DHAS_deepseq if flag(hashable) build-depends: hashable other-modules: Exinst.Instances.Hashable + cpp-options: -DHAS_hashable if flag(quickcheck) build-depends: QuickCheck other-modules: Exinst.Instances.QuickCheck - + cpp-options: -DHAS_quickcheck + if flag(serialise) + build-depends: cborg, serialise + other-modules: Exinst.Instances.Serialise + cpp-options: -DHAS_serialise test-suite tests default-language: Haskell2010 type: exitcode-stdio-1.0 - hs-source-dirs: tests src/lib + hs-source-dirs: tests lib main-is: Main.hs build-depends: aeson @@ -66,17 +76,27 @@ , binary , bytes , bytestring + , cborg , cereal , constraints , deepseq , hashable , profunctors , QuickCheck + , serialise , singletons , tasty , tasty-hunit , tasty-quickcheck - + cpp-options: + -DHAS_aeson + -DHAS_binary + -DHAS_bytes + -DHAS_cereal + -DHAS_deepseq + -DHAS_hashable + -DHAS_quickcheck + -DHAS_serialise flag aeson description: Provide instances for @aeson@ @@ -104,5 +124,9 @@ manual: True flag quickcheck description: Provide instances for @QuickCheck@ + default: True + manual: True +flag serialise + description: Provide instances for @serialise@ default: True manual: True diff --git a/lib/Exinst.hs b/lib/Exinst.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst.hs @@ -0,0 +1,685 @@ +{-# LANGUAGE CPP #-} + +{- | + +Exinst is a library providing you with tools to recover type-indexed types whose +type-indexes have been existentialized, as well as automatically deriving +instances for them, as long as said type indexes are singleton types +(see [singleton](https://hackage.haskell.org/package/singletons)). + +In short, what @exinst@ currently gives you is: For any type @t :: k -> *@, if +@k@ is a singleton type and @c (t a) :: 'Constraint'@ is satisfied, then you can +existentialize away the @a@ parameter with @'Some1' t@, recover it later, and +have @c ('Some1' t)@ automatically satisfied. Currently, up to 4 type indexes +can be existentialized using 'Some1', 'Some2', 'Some3' and 'Some4' respectively. + +NOTE: This tutorial asumes some familiarity with singleton types as implemented +by the [singleton](https://hackage.haskell.org/package/singletons) library. +A singleton type is, in very rough terms, a type inhabited by a single term, +which allows one to go from its term-level representation to its type-level +representation and back without much trouble. A bit like the term @()@, which +is of type @()@. Whenever you have the type @()@ you know what that its +term-level representation must be @()@, and whenever you have the term @()@ +you know that its type must be @()@. + +-} + +module Exinst + ( -- * Tutorial + -- $motivation + + -- *** Usage + -- $usage + + -- *** Recovering + -- $recovering + + -- *** Many indexes + -- $manyIndexes + + -- *** Writing instances + -- $writingInstances + + -- *** Products and sums + -- $prodsums + + -- * 1 type index + Some1(Some1) + , some1 + , fromSome1 + , _Some1 + , withSome1 + , withSome1Sing + , some1SingRep + , same1 + , Dict1(dict1) + + -- * 2 type indexes + , Some2(Some2) + , some2 + , fromSome2 + , _Some2 + , withSome2 + , withSome2Sing + , some2SingRep + , same2 + , Dict2(dict2) + + -- * 3 type indexes + , Some3(Some3) + , some3 + , fromSome3 + , _Some3 + , withSome3 + , withSome3Sing + , some3SingRep + , same3 + , Dict3(dict3) + + -- * 4 type indexes + , Some4(Some4) + , some4 + , fromSome4 + , _Some4 + , withSome4 + , withSome4Sing + , some4SingRep + , same4 + , Dict4(dict4) + + -- * Miscellaneous + , Dict0(dict0) + + -- * Products + , P1(P1) + , P2(P2) + , P3(P3) + , P4(P4) + + -- * Sums + , S1(S1L,S1R) + , S2(S2L,S2R) + , S3(S3L,S3R) + , S4(S4L,S4R) + + -- * Re-exports + , Constraint + , Dict(Dict) + , Sing + , SingI + ) where + +import Data.Constraint (Constraint, Dict(Dict)) + +import Data.Singletons (Sing, SingI) + +import Exinst.Internal +import Exinst.Internal.Product +import Exinst.Internal.Sum + +import Exinst.Instances.Base () + +#ifdef HAS_aeson +import Exinst.Instances.Aeson () +#endif + +#ifdef HAS_binary +import Exinst.Instances.Binary () +#endif + +#ifdef HAS_bytes +import Exinst.Instances.Bytes () +#endif + +#ifdef HAS_cereal +import Exinst.Instances.Cereal () +#endif + +#ifdef HAS_deepseq +import Exinst.Instances.DeepSeq () +#endif + +#ifdef HAS_hashable +import Exinst.Instances.Hashable () +#endif + +#ifdef HAS_quickcheck +import Exinst.Instances.QuickCheck () +#endif + +#ifdef HAS_serialise +import Exinst.Instances.Serialise () +#endif + + +{- $motivation + +As a motivation, let's consider the following example: + +@ +\{\-\# LANGUAGE GADTs \#\-\} +\{\-\# LANGUAGE DataKinds \#\-\} +\{\-\# LANGUAGE KindSignatures \#\-\} +\{\-\# LANGUAGE FlexibleInstances \#\-\} +\{\-\# LANGUAGE StandaloneDeriving \#\-\} + +data Size = Big | Small + +data Receptacle (a :: Size) :: * where + Vase :: Receptacle 'Small + Glass :: Receptacle 'Small + Barrel :: Receptacle 'Big + +deriving instance 'Show' (Receptacle a) +@ + +@Receptacle@ can describe three types of receptacles (@Vase@, @Glass@ and +@Barrel@), while at the same time being able to indicate, at the type level, +whether the size of the receptacle is @Big@ or @Small@. Additionally, we've +provided 'Show' instances for @Receptacle@. + +Now, if we want to put @Receptacle@s in a container, for example in @[]@, we can +do so only as long as the @Receptacle@ type is fully applied and monomorphic. +That is, we can have @[Receptacle 'Small]@ and @[Receptacle 'Big]@, but we +can't have @[Receptacle]@ nor @[forall a. Receptacle a]@. So, if we want to +have @Receptacle@s of different sizes in a container like @[]@, we need a +different solution. + +At this point we need to ask ourselves why we need to put @Receptacle@s of +different sizes in a same container. If the answer is something like “because we +want to show all of them, no matter what size they are”, then we should realize +that what we are actually asking for is that no matter what @Size@ our +@Receptable@ has, we need to be able to find a 'Show' instance for that +@Receptacle@. In Haskell, we can express just that using existential types +and constraints hidden behind a data constructor. + +@ +-- We need to add these language extensions to the ones in the previous example +\{\-\# LANGUAGE ExistentialQuantification \#\-\} +\{\-\# LANGUAGE FlexibleContexts \#\-\} + +data ReceptacleOfAnySizeThatCanBeShown + = forall a. ('Show' (Receptacle a)) + => MkReceptacleOfAnySizeThatCanBeShown (Receptacle a) +@ + +We can construct values of type @ReceptacleOfAnySizeThatCanBeShown@ only as long +as there exist a 'Show' instance for the @Receptacle a@ we give to the +@MkReceptacleOfAnySizeThatCanBeShown@ constructor. In our case, both @Receptacle +'Small@ and @Receptacle 'Big@ have 'Show' instances, so all of @Vase@, @Glass@ and +@Barrel@ can be used successfully with @MkReceptacleOfAnySizeThatCanBeShown@. + +Now, @ReceptacleOfAnySizeThatCanBeShown@ on itself doesn't yet have a 'Show' +instance, and we can't derive one automatically using the @deriving@ mechanism, +but we can give an explicit 'Show' instance that just forwards the work to the +'Show' instance of the underlying @Receptacle a@. + +@ +instance 'Show' ReceptacleOfAnySizeThatCanBeShown where + 'show' (MkReceptacleOfAnySizeThatCanBeShown a) = 'show' a +@ + +That works as intended: + +@ +> 'show' (MkReceptacleOfAnySizeThatCanBeShown Vase) +"Vase" +> 'show' (MkReceptacleOfAnySizeThatCanBeShown Barrel) +"Barrel" +@ + +And now, as we wanted, we can put @Receptacle@s of different sizes in a @[]@ and +show them (as long as we wrap each of them as +@ReceptacleOfAnySizeThatCanBeShown@, that is). + +@ +> 'map' 'show' [MkReceptacleOfAnySizeThatCanBeShown Vase, MkReceptacleOfAnySizeThatCanBeShown Barrel] +["Vase", "Barrel"] +@ + +However, the above solution is unsatisfying for various reasons: For one, the +'Show' instance for @ReceptacleOfAnySizeThatCanBeShown@ works only as long as +the @ReceptacleOfAnySizeThatCanBeShown@ itself carries a witness that the 'Show' +constraint for @Receptacle a@ is satisfied, which means that if we want to write +yet another instance for @ReceptacleOfAnySizeThatCanBeShown@ that simply forwards +its implementation to the underlying @Receptacle a@, say 'Eq', then the +@MkReceptacleOfAnySizeThatCanBeShown@ constructor would need to be modified to witness +the @Eq (Receptacle a)@ instance too: + +@ +data ReceptacleOfAnySizeThatCanBeShown + = forall a. ('Show' (Receptacle a), 'Eq' (Receptacle a)) + => MkReceptacleOfAnySizeThatCanBeShown (Receptacle a) +@ + +With that in place we can provide an 'Eq' instance for +@ReceptacleOfAnySizeThatCanBeShown@ as we did for 'Show' before, but if we pay +close attention, we can see how the implementation of +@ReceptacleOfAnySizeThatCanBeShown@ starts to become a bottleneck: Every +instance we want to provide for @ReceptacleOfAnySizeThatCanBeShown@ that simply +forwards its work to the underlying @Receptacle a@ needs to be witnessed by +@MkReceptacleOfAnySizeThatCanBeShown@ itself, it is not enough that there exists +an instance for @Receptacle a@. Moreover, even the name +@ReceptacleOfAnySizeThatCanBeShown@ that we chose before isn't completely +accurate anymore, and will become less and less accurate as we continue adding +constraints to @MkReceptacleOfAnySizeThatCanBeShown@. + +Additionally, everywhere we use the @MkReceptacleOfAnySizeThatCanBeShown@ +constructor we need to witness that the existentialized @Receptacle a@ satisfies +all the required constraints, which means that, if the @Receptacle a@ we pass to +@MkReceptacleOfAnySizeThatCanBeShown@ is being received, say, as a parameter to +a function, then the type of that function will also require that its caller +satisfies all of the same constraints, even though it is obvious to us, +statically, that the instances exist. We can now see how all of this becomes +unmanegeable, or at least very *boilerplatey*, as those constraints start to +propagate through our code base. + +What we need is a way for instances such as the 'Show' instance for +@ReceptacleOfAnySizeThatCanBeShown@ to find the 'Show' instance for @Receptacle +a@ without it being explicitely witnessed by the +@MkReceptacleOfAnySizeThatCanBeShown@ constructor. That is exactly the problem +that @exinst@ solves: allowing /exi/stentials to find their /inst/ances. Thus, +the name of this library. + +-} + +{- $usage + +Given the code for @Size@, @Receptacle@ and its 'Show' instances above, we can +achieve the same functionality as our initial @ReceptacleOfAnySizeThatCanBeShown@ by +existentializing the type indexes of @Receptacle 'Small@ and @Receptacle 'Big@ +as @'Some1' Receptacle@. In order to do that, we must first ensure that @Size@ and its +constructors can be used as singleton types (as supported by the @singletons@ library), +for which we can use some @TemplateHaskell@ provided by @Data.Singletons.TH@: + +@ +import qualified "Data.Singletons.TH" + +Data.Singletons.TH.genSingletons [''Size] +@ + +And we'll also need a 'Show' instance for @Size@ for reasons that will become +apparent later: + +@ +deriving instance 'Show' Size +@ + +Now we can construct a @Show1 Size@ and 'show' achieving the same results as we +did with @ReceptacleOfAnySizeThatCanBeShown@ before. + +Note: this code won't work yet. Keep reading. + +@ +> import "Exinst" ('Some1', 'some1') +> :t 'some1' Glass +:t 'some1' Glass :: 'Some1' Receptacle +> 'show' ('some1' Glass) +"Some1 Small Glass" +@ + +Well, actually, the default 'Show' instance for 'Some1' shows a bit more of +information, as it permits this string to be 'Read' back into a @'Some1' +Receptacle@ if needed, but displaying just @"Glass"@ would be possible too, if +desired. + +The important thing to notice in the example above is that @some1@ does not +require us to satisfy a @'Show' (Receptacle 'Small)@ constraint, it just requires +that the type index for the type-indexed type we give it as argument is a +singleton type: + +@ +'some1' :: forall (f1 :: k1 -> *) (a1 :: k1). 'SingI' a1 => f1 a1 -> 'Some1' f1 +@ + +It is the application of 'show' to @'some1' Glass@ which will fail to compile if +there isn't a 'Show' instance for @Receptacle 'Small@, complaining that a 'Show' +instance for @'Some1' Receptable@ can't be found. The reason for this is that even +if 'Show' instances for 'Some1' are derived for free, they are only derived for +@'Some1' (t :: k1 -> *)@ where a @'Show' (t a)@ for a specific but statically +unknown @a@ can be found at runtime (mostly, there are other minor requirements too). +The mechanism through which instances are found at runtime relies on 'Dict' from +the [constraints](https://hackage.haskell.org/package/constraints) library, which +@exinst@ wraps in a 'Dict1' typeclass to be instantiated once per singleton +type. + +@ +-- The "Exinst.Dict1" class +class 'Dict1' (c :: k0 -> 'Constraint') (f1 :: k1 -> k0) where + 'dict1' :: 'Sing' (a1 :: k1) -> 'Dict' (c (f1 a1)) +@ + +What 'Dict1' says is that: for a type-indexed type @f1@, given a term-level +representation of the singleton type that indexes said @f1@, we can obtain a +witness that the constraint @c@ is satisfied by @f1@ applied to the singleton +type. + +That class seems to be a bit too abstract, but the instances we as users need to +write for it are quite silly and straightforward. + +Here's an example of how to provide 'Show' support for @'Some1' Receptacle@ via +'Dict1': + +@ +instance ('Show' (Receptacle 'Small), 'Show' (Receptacle 'Big)) => 'Dict1' 'Show' Receptacle where + 'dict1' = \x -> case x of + SSmall -> 'Dict' + SBig -> 'Dict' +@ + +The implementation of @dict1@ looks quite silly, but it has to look like that as +it is only by pattern-matching on each of the @'Sing' Size@ constructors that we +learn about the type level representation of a singleton type, which we then use +to select the proper 'Show' instance among all of those listed in the instance head. + +Given this 'Dict1' instance, we can proceed to excecute the REPL example mentioned before +and it will work just fine. + +However, that 'Dict1' instance is still a bit insatisfactory: If we wanted, +again, to provide 'Eq' support for our @'Some1' Receptacle@ type, we would need to +write yet another 'Dict1' instance like the one above, but mentioning 'Eq' +instead of 'Show'. We can do better. + +The trick, when writing 'Dict1' instances such as the one above, is to leave @c@ +and @f1 :: k1 -> k0@ completely polymorphic, and instead only talk concretely +about the singleton type with kind @k1@. This might sound strange at first, as +@c@ and @f1@ are the only two type parameters to 'Dict1'. But as it often happens +when working with singleton types, we are not particularly interested in the +types involved, but in their kinds instead. So, this is the 'Dict1' instance +you often want to write: + +@ +instance (c (f1 'Small), c (f1 'Big)) => 'Dict1' c (f1 :: Size -> k0) where + 'dict1' = \x -> case x of + SSmall -> 'Dict' + SBig -> 'Dict' +@ + +That instance says that for any choice of @c@ and @f1 :: Size -> k0@, if an +instance for @c (f1 a)@ exists for a specific choice of @a@, then, given a term +level representation for that @a@ and the aid of @dict1@, said instance can be +looked up at runtime. + +Notice that 'Some1' itself doesn't have any requirements about 'Dict1', it's the +various instances for 'Some1' who rely on 'Dict1'. 'Dict1' has nothing to do +with 'Some1', nor with the choice of @f@ nor with the choice of @c@; it is only +related to the singleton type used as a type-index for @f@. + +The @Exinst@ module exports ready-made instances for 'Some1', 'Some2', 'Some3' +and 'Some4' (they can be enabled or disabled with some cabal flags). + +* 'Eq', 'Ord', 'Show' from the @base@ package. + +* 'Data.Aeson.FromJSON' and 'Data.Aeson.ToJSON' from the @aeson@ package. + +* 'Data.Bytes.Serial' from the @bytes@ package. + +* 'Cereal.Serialize.Serialize' from the @cereal@ package. + +* 'Data.Binary.Binary' from the @binary@ package. + +* 'Data.Hashable.Hashable' from the @hashable@ package. + +* 'Control.DeepSeq.NFData' from the @deepseq@ package. + +* 'Test.QuickCheck.Arbitrary' from the @QuickCheck@ package. + +You are invited to read the instance heads for said instances so as to understand +what you need to provide in order to get those instances “for free”. As a rule of +thumb, most instances will require this: If you expect to have an instance for +@class Y => Z a@ satisfied for @'Some1' (f :: k1 -> *)@, then make sure an instance +for @Z@ is available for the @DemoteRep k1@, that a @'Dict1' Z (f :: k1 -> k0)@ or +more general instance exists, and that the @Y@ instance for @'Some1' (f :: k1 -> +*)@ exists too. + +Here is the full code needed to have, say, the 'Eq' and 'Show' instances +available for @'Some1' Receptacle@: + +@ +\{\-\# LANGUAGE ConstraintKinds \#\-\} +\{\-\# LANGUAGE DataKinds \#\-\} +\{\-\# LANGUAGE FlexibleInstances \#\-\} +\{\-\# LANGUAGE GADTs \#\-\} +\{\-\# LANGUAGE KindSignatures \#\-\} +\{\-\# LANGUAGE MultiParamTypeClasses \#\-\} +\{\-\# LANGUAGE OverloadedStrings \#\-\} +\{\-\# LANGUAGE StandaloneDeriving \#\-\} +\{\-\# LANGUAGE TemplateHaskell \#\-\} +\{\-\# LANGUAGE TypeFamilies \#\-\} +\{\-\# LANGUAGE UndecidableInstances \#\-\} + +import qualified "Data.Singletons.TH" +import "Exinst" ('Dict'('Dict'), 'Dict1'('dict1')) + +data Size = Big | Small + deriving ('Eq', 'Show') + +Data.Singletons.TH.genSingletons [''Size] +Data.Singletons.TH.singDecideInstances [''Size] + +instance (c (f 'Big), c (f 'Small)) => 'Dict1' c f where + 'dict1' = \x -> case x of + SBig -> 'Dict' + SSmall -> 'Dict' + + +data Receptacle (a :: Size) :: * where + Vase :: Receptacle 'Small + Glass :: Receptacle 'Small + Barrel :: Receptacle 'Big + +deriving instance 'Eq' (Receptacle a) +deriving instance 'Show' (Receptacle a) +@ + +Now, @'Some1' Receptacle@ will have 'Eq' and 'Show' instances: + +@ +> -- Trying 'fromSome1'. +> 'fromSome1' ('some1' Vase) == 'Just' Vase +'True' +> 'fromSome1' ('some1' Vase) == 'Just' Glass +'False' +> 'fromSome1' ('some1' Vase) == 'Just' Barrel +'False' + +> -- Trying 'withSome1' +> 'withSome1' ('some1' Vase) 'show' +"Vase" +> 'withSome1' ('some1' Vase) (== Vase) -- This will fail, use 'fromSome1' + -- if you know you are expecting + -- a @Receptacle 'Small@ + +> -- Trying the 'Eq' instance. +> 'some1' Vase == 'some1' Vase +'True' +> 'some1' Vase == 'some1' Glass +'False' +> 'some1' Vase == 'some1' Barrel +'False' + +> -- Trying the 'Show' instance. +> 'show' ('some1' Vase) +"Some1 Small Vase" +> 'map' 'show' ['some1' Vase, 'some1' Glass, 'some1' Barrel] +["Some1 Small Vase","Some1 Small Glass","Some1 Big Barrel"] +@ + +-} + +{- $manyIndexes + +Just like 'Some1' hides the last singleton type index from fully applied +type-indexed type, 'Some2' hides the last two type indexes, 'Some3' hides the +last three, and 'Some3' hides the last four. They can be used in the same way as +'Some1'. + +Like as most instances for 'Some1' require 'Dict1' instances to be present for +their singleton type-index, most instances for 'Some2', 'Some3' and 'Some4' will +require that 'Dict2', 'Dict3' or 'Dict4' instances exist, respectively. Writing +these instances is very straightforward. Supposing you have a type @X :: T4 -> +T3 -> T2 -> T1 -> *@ and want to existentialize all of the four type indexes yet +be able to continue using all of its instances, we can write something like +this: + +@ +instance (c (f1 'T1a), c (f1 'T1b)) => 'Dict1' c (f1 :: T1 -> k0) where + 'dict1' = \x -> case x of { ST1a -> 'Dict'; ST1b -> 'Dict' } +instance ('Dict1' c (f2 'T2a), 'Dict1' c (f2 'T2b)) => 'Dict2' c (f2 :: T2 -> k1 -> k0) where + 'dict2' = \x -> case x of { ST2a -> 'dict1'; ST2b -> 'dict1' } +instance ('Dict2' c (f3 'T3a), 'Dict2' c (f3 'T3b)) => 'Dict3' c (f3 :: T3 -> k2 -> k1 -> k0) where + 'dict3' = \x -> case x of { ST3a -> 'dict2'; ST3b -> 'dict2' } +instance ('Dict3' c (f4 'T4a), 'Dict3' c (f4 'T4b)) => 'Dict4' c (f4 :: T4 -> k3 -> k2 -> k1 -> k0) where + 'dict4' = \x -> case x of { ST4a -> 'dict3'; ST4b -> 'dict3' } +@ + +That is, assuming the following @T1@, @T2@, @T3@ and @T4@: + +@ +data T4 = T4a | T4b +data T3 = T3a | T3b +data T2 = T2a | T2b +data T1 = T1a | T1b +@ + +Effectively, we wrote just one instance per singleton type per type-index +position, each of them promoting a term-level representation of a singleton +type to its type-level representation and forwarding the rest of the work to +a “smaller” dict. That is, 'dict4' reifies the type of the fourth-to-last +type-index of @X@ and then calls 'dict3' to do the same for the third-to-last +type-index of @X@ and so on. Notice, however, how we didn't need to mention @X@ +in none of the instances above: As we said before, these instances are +intended to work for any choice of @c@, @f4@, @f3@, @f2@ and @f1@. + +-} + +{- $recovering + +If you have a @'Some1' (f :: k -> *)@ and you know, statically, that you need an +specific @f (a :: k)@, then you can use 'fromSome1' which will give you an +@f (a :: k)@ only if @a@ was the type that was existentialized by 'Some1'. +Using 'fromSome1' requires that the singleton type-index implements +'Data.Singletons.Decide.SDecide', which can be derived mechanically with +`TemplateHaskell` by means of 'Data.Singletons.TH.singInstance'. + +If you don't know, statically, the type of @f (a :: k)@, then you can use +'withSome1Sing' or 'withSome1' to work with @f (a :: k)@ as long as @a@ never +leaves their scope (don't worry, the compiler will yell at you if you try to do +that). + +-} + + +{- $prodsums + +Consider the following types and constructors: + +@ +data X (a :: 'Bool') where + XT :: X ''True' + XF :: X ''False' + +data Y (a :: 'Bool') where + YT :: Y ''True' + YF :: Y ''False' +@ + +You can use '(,)' to create a product for values of this type, and 'Either' to +create a sum. However, see what happens if we try to existentialize the type +index when using that approach: + +@ +> :t ('some1' XT, 'some1' YT) +('some1' XT, 'some1' YT) :: ('Some1' X, 'Some1' Y) +> :t ('some1' XT, 'some1' YF) +('some1' XT, 'some1' YF) :: ('Some1' X, 'Some1' Y) +@ + +It works, but there is no type level guarantee that the type index taken by @X@ +and @Y@ is the same. If you do want to enforce that restriction, then you can +use @P1@ instead: + +@ +> :t 'P1' +'P1' :: l a -> r a -> 'P1' l r (a :: k) +> :t 'P1' XT YT +'P1' XT YT :: 'P1' X Y ''True' +> :t 'P1' XT YT +'P1' XT YT :: 'P1' X Y ''True' +> :t 'some1' ('P1' XT YT) +'some1' ('P1' XT YT) :: 'Some1' ('P1' X Y) +@ + +Trying to mix @XT@ with @YF@ fails, of course, since they have different type +indexes: + +@ +> :t 'P1' XT YF +\:1:7: error: + • Couldn't match type ‘''False'’ with ‘''True'’ + Expected type: Y ''True' + Actual type: Y ''False' + • In the second argument of ‘'P1'’, namely ‘YF’ + In the expression: 'P1' XT YF +@ + +Moreover, 'P1' supports many common instances from @base@, @hashable@, +@deepseq@, @aeson@, @bytes@, @cereal@, @binary@ and @quickcheck@ out of the +box, so you can benefit from them as well. + +There's also 'P2', 'P3' and 'P4' for product types taking a different number of +indexes, and also 'S1', 'S2', 'S3' and 'S4' for sum types: + +@ +> :t 'S1L' +'S1L' :: l a -> 'S1' l r (a :: k) +> :t 'S1R' +'S1R' :: r a -> 'S1' l r (a :: k) +> :t 'S1L' XT +'S1L' XT :: 'S1' X r ''True' +> :t 'S1R' YT +'S1R' YT :: 'S1' l Y ''True' +> :t 'some1' ('S1L' XT) +'some1' ('S1L' XT) :: 'Some1' ('S1' X r) +> :t 'some1' ('S1R' YT) +'some1' ('S1R' YT) :: 'Some1' ('S1' l Y) +@ + +-} + + +{- $writingInstances + +Instances for 'Some1' seem to come out of thin air, but the truth is that they +need to be written at least once by library authors so that, provided all its +requirements are satisfied, they are made available. + +For example, when we imported "Exinst" before, we also brought to scope, among +other things, the 'Eq' instance for 'Some1', which is defined as this: + +@ +instance forall (f :: k1 -> *). + ( 'Data.Singletons.Decide.SDecide' k1 + , 'Dict1' 'Eq' f + ) => 'Eq' ('Some1' f) + where + (==) = \\som1x som1y -> + 'withSome1Sing' som1x $ \\sa1x (x :: f a1x) -> + 'withSome1Sing' som1y $ \\sa1y (y :: f a1y) -> + 'maybe' 'False' 'id' $ do + 'Data.Type.Equality.Refl' <- 'Data.Type.Equality.testEquality' sa1x sa1y + case 'dict1' sa1x :: 'Dict' ('Eq' (f a1x)) of + 'Dict' -> 'Just' (x == y) +@ + +This code should be relatively straightforward if you are familiar with uses of +the @singletons@ and @constraints@ libraries. We are simply reifying singleton +types from their term-level representation to their type-level representation, +and afterwards using the 'Dict1' mechanism to lookup the required instances +during runtime. Additionaly, this instance requires that the term level +representation of the singleton type implements 'Show' too, as, like we saw in a +previous example, the type index itself is shown in this 'Show' implementation, +in the hope that it can be later recovered and reified to the type level when +using 'Read'. + +-} diff --git a/lib/Exinst/Instances/Aeson.hs b/lib/Exinst/Instances/Aeson.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Instances/Aeson.hs @@ -0,0 +1,159 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'Ae.FromJSON' and 'Ae.ToJSON' instances for 'Some1', +-- 'Some2', 'Some3' and 'Some4' from "Exinst", provided situable +-- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available. +-- +-- See the README file in the @exinst@ package for more general documentation: +-- https://hackage.haskell.org/package/exinst#readme +module Exinst.Instances.Aeson () where + +import qualified Data.Aeson as Ae +import Data.Constraint +import Data.Singletons +import Prelude + +import Exinst.Internal + +-------------------------------------------------------------------------------- + +instance forall (f :: k1 -> *) + . ( SingKind k1 + , Ae.ToJSON (Demote k1) + , Dict1 Ae.ToJSON f + ) => Ae.ToJSON (Some1 f) + where + {-# INLINABLE toJSON #-} + toJSON = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (Ae.ToJSON (f a1)) of + Dict -> Ae.toJSON (fromSing sa1, x) + +instance forall (f :: k2 -> k1 -> *) + . ( SingKind k2 + , SingKind k1 + , Ae.ToJSON (Demote k2) + , Ae.ToJSON (Demote k1) + , Dict2 Ae.ToJSON f + ) => Ae.ToJSON (Some2 f) + where + {-# INLINABLE toJSON #-} + toJSON = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (Ae.ToJSON (f a2 a1)) of + Dict -> Ae.toJSON ((fromSing sa2, fromSing sa1), x) + +instance forall (f :: k3 -> k2 -> k1 -> *) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , Ae.ToJSON (Demote k3) + , Ae.ToJSON (Demote k2) + , Ae.ToJSON (Demote k1) + , Dict3 Ae.ToJSON f + ) => Ae.ToJSON (Some3 f) + where + {-# INLINABLE toJSON #-} + toJSON = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f a3 a2 a1)) of + Dict -> Ae.toJSON ((fromSing sa3, fromSing sa2, fromSing sa1), x) + +instance forall (f :: k4 -> k3 -> k2 -> k1 -> *) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , Ae.ToJSON (Demote k4) + , Ae.ToJSON (Demote k3) + , Ae.ToJSON (Demote k2) + , Ae.ToJSON (Demote k1) + , Dict4 Ae.ToJSON f + ) => Ae.ToJSON (Some4 f) + where + {-# INLINABLE toJSON #-} + toJSON = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f a4 a3 a2 a1)) of + Dict -> Ae.toJSON ((fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1), x) + +-------------------------------------------------------------------------------- + +instance forall (f :: k1 -> *) + . ( SingKind k1 + , Ae.FromJSON (Demote k1) + , Dict1 Ae.FromJSON f + ) => Ae.FromJSON (Some1 f) + where + {-# INLINABLE parseJSON #-} + parseJSON = \v -> do + (rsa1, v') <- Ae.parseJSON v + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (Ae.FromJSON (f a1)) of + Dict -> do + x :: f a1 <- Ae.parseJSON v' + pure (Some1 sa1 x) + +instance forall (f :: k2 -> k1 -> *) + . ( SingKind k2 + , SingKind k1 + , Ae.FromJSON (Demote k2) + , Ae.FromJSON (Demote k1) + , Dict2 Ae.FromJSON f + ) => Ae.FromJSON (Some2 f) + where + {-# INLINABLE parseJSON #-} + parseJSON = \v -> do + ((rsa2, rsa1), v') <- Ae.parseJSON v + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict2 sa2 sa1 :: Dict (Ae.FromJSON (f a2 a1)) of + Dict -> do + x :: f a2 a1 <- Ae.parseJSON v' + pure (Some2 sa2 sa1 x) + +instance forall (f :: k3 -> k2 -> k1 -> *) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , Ae.FromJSON (Demote k3) + , Ae.FromJSON (Demote k2) + , Ae.FromJSON (Demote k1) + , Dict3 Ae.FromJSON f + ) => Ae.FromJSON (Some3 f) + where + {-# INLINABLE parseJSON #-} + parseJSON = \v -> do + ((rsa3, rsa2, rsa1), v') <- Ae.parseJSON v + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict3 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f a3 a2 a1)) of + Dict -> do + x :: f a3 a2 a1 <- Ae.parseJSON v' + pure (Some3 sa3 sa2 sa1 x) + +instance forall (f :: k4 -> k3 -> k2 -> k1 -> *) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , Ae.FromJSON (Demote k4) + , Ae.FromJSON (Demote k3) + , Ae.FromJSON (Demote k2) + , Ae.FromJSON (Demote k1) + , Dict4 Ae.FromJSON f + ) => Ae.FromJSON (Some4 f) + where + {-# INLINABLE parseJSON #-} + parseJSON = \v -> do + ((rsa4, rsa3, rsa2, rsa1), v') <- Ae.parseJSON v + withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f a4 a3 a2 a1)) of + Dict -> do + x :: f a4 a3 a2 a1 <- Ae.parseJSON v' + pure (Some4 sa4 sa3 sa2 sa1 x) diff --git a/lib/Exinst/Instances/Base.hs b/lib/Exinst/Instances/Base.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Instances/Base.hs @@ -0,0 +1,622 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'Show', 'Eq' and 'Ord' instances for 'Exinst.Some1', +-- 'Exinst.Some2', 'Exinst.Some3' and 'Exinst.Some4' from "Exinst", provided situable +-- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available. +-- +-- See the README file for more general documentation: https://hackage.haskell.org/package/exinst#readme +module Exinst.Instances.Base () where + +import Data.Constraint +import Data.Kind (Type) +import Data.Singletons +import Data.Singletons.Prelude.Enum (PEnum(EnumFromTo), PBounded(MinBound, MaxBound)) +import Data.Singletons.Prelude.Bool (Sing(STrue,SFalse)) +import qualified Data.Singletons.Prelude.List as List +import Data.Singletons.Prelude.Tuple (Tuple2Sym1) +import Data.Singletons.Decide +import Data.Type.Equality +import qualified GHC.Generics as G +import Prelude +import qualified Text.Read as Read + +import Exinst.Internal + hiding (Some1(..), Some2(..), Some3(..), Some4(..)) +import qualified Exinst.Internal as Exinst + +-------------------------------------------------------------------------------- +-- Show + +-- Internal wrappers used to avoid writing the string manipulation in 'Show'. +data Some1'Show r1 x = Some1 r1 x deriving (Show) +data Some2'Show r2 r1 x = Some2 r2 r1 x deriving (Show) +data Some3'Show r3 r2 r1 x = Some3 r3 r2 r1 x deriving (Show) +data Some4'Show r4 r3 r2 r1 x = Some4 r4 r3 r2 r1 x deriving (Show) + +instance forall (f :: k1 -> Type) + . ( SingKind k1 + , Show (Demote k1) + , Dict1 Show f + ) => Show (Exinst.Some1 f) + where + {-# INLINABLE showsPrec #-} + showsPrec n = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (Show (f a1)) of + Dict -> showsPrec n (Some1 (fromSing sa1) x) + +instance forall (f :: k2 -> k1 -> Type) + . ( SingKind k2 + , SingKind k1 + , Show (Demote k2) + , Show (Demote k1) + , Dict2 Show f + ) => Show (Exinst.Some2 f) + where + {-# INLINABLE showsPrec #-} + showsPrec n = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (Show (f a2 a1)) of + Dict -> showsPrec n (Some2 (fromSing sa2) (fromSing sa1) x) + +instance forall (f :: k3 -> k2 -> k1 -> Type) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , Show (Demote k3) + , Show (Demote k2) + , Show (Demote k1) + , Dict3 Show f + ) => Show (Exinst.Some3 f) + where + {-# INLINABLE showsPrec #-} + showsPrec n = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (Show (f a3 a2 a1)) of + Dict -> showsPrec n (Some3 (fromSing sa3) (fromSing sa2) (fromSing sa1) x) + +instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , Show (Demote k4) + , Show (Demote k3) + , Show (Demote k2) + , Show (Demote k1) + , Dict4 Show f + ) => Show (Exinst.Some4 f) + where + {-# INLINABLE showsPrec #-} + showsPrec n = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Show (f a4 a3 a2 a1)) of + Dict -> showsPrec n (Some4 (fromSing sa4) (fromSing sa3) + (fromSing sa2) (fromSing sa1) x) + +-------------------------------------------------------------------------------- +-- Read + +instance forall (f :: k1 -> Type) + . ( SingKind k1 + , Read (Demote k1) + , Dict1 Read f + ) => Read (Exinst.Some1 f) + where + {-# INLINABLE readPrec #-} + readPrec = do + Read.Ident "Some1" <- Read.lexP + rsa1 <- Read.readPrec + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (Read (f a1)) of + Dict -> do + x :: f a1 <- Read.readPrec + pure (Exinst.Some1 sa1 x) + +instance forall (f :: k2 -> k1 -> Type) + . ( SingKind k2 + , SingKind k1 + , Read (Demote k2) + , Read (Demote k1) + , Dict2 Read f + ) => Read (Exinst.Some2 f) + where + {-# INLINABLE readPrec #-} + readPrec = do + Read.Ident "Some2" <- Read.lexP + rsa2 <- Read.readPrec + rsa1 <- Read.readPrec + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict2 sa2 sa1 :: Dict (Read (f a2 a1)) of + Dict -> do + x :: f a2 a1 <- Read.readPrec + pure (Exinst.Some2 sa2 sa1 x) + +instance forall (f :: k3 -> k2 -> k1 -> Type) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , Read (Demote k3) + , Read (Demote k2) + , Read (Demote k1) + , Dict3 Read f + ) => Read (Exinst.Some3 f) + where + {-# INLINABLE readPrec #-} + readPrec = do + Read.Ident "Some3" <- Read.lexP + rsa3 <- Read.readPrec + rsa2 <- Read.readPrec + rsa1 <- Read.readPrec + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict3 sa3 sa2 sa1 :: Dict (Read (f a3 a2 a1)) of + Dict -> do + x :: f a3 a2 a1 <- Read.readPrec + pure (Exinst.Some3 sa3 sa2 sa1 x) + +instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , Read (Demote k4) + , Read (Demote k3) + , Read (Demote k2) + , Read (Demote k1) + , Dict4 Read f + ) => Read (Exinst.Some4 f) + where + {-# INLINABLE readPrec #-} + readPrec = do + Read.Ident "Some4" <- Read.lexP + rsa4 <- Read.readPrec + rsa3 <- Read.readPrec + rsa2 <- Read.readPrec + rsa1 <- Read.readPrec + withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Read (f a4 a3 a2 a1)) of + Dict -> do + x :: f a4 a3 a2 a1 <- Read.readPrec + pure (Exinst.Some4 sa4 sa3 sa2 sa1 x) + +-------------------------------------------------------------------------------- +-- Eq + +instance forall (f :: k1 -> Type). + ( SDecide k1 + , Dict1 Eq f + ) => Eq (Exinst.Some1 f) + where + {-# INLINABLE (==) #-} + (==) = \som1x som1y -> + withSome1Sing som1x $ \sa1x (x :: f a1x) -> + withSome1Sing som1y $ \sa1y (y :: f a1y) -> + maybe False id $ do + Refl <- testEquality sa1x sa1y + case dict1 sa1x :: Dict (Eq (f a1x)) of + Dict -> Just (x == y) + +instance forall (f :: k2 -> k1 -> Type) + . ( SDecide k2 + , SDecide k1 + , Dict2 Eq f + ) => Eq (Exinst.Some2 f) + where + {-# INLINABLE (==) #-} + (==) = \som2x som2y -> + withSome2Sing som2x $ \sa2x sa1x (x :: f a2x a1x) -> + withSome2Sing som2y $ \sa2y sa1y (y :: f a2y a1y) -> + maybe False id $ do + Refl <- testEquality sa2x sa2y + Refl <- testEquality sa1x sa1y + case dict2 sa2x sa1x :: Dict (Eq (f a2x a1x)) of + Dict -> Just (x == y) + +instance forall (f :: k3 -> k2 -> k1 -> Type) + . ( SDecide k3 + , SDecide k2 + , SDecide k1 + , Dict3 Eq f + ) => Eq (Exinst.Some3 f) + where + {-# INLINABLE (==) #-} + (==) = \som3x som3y -> + withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f a3x a2x a1x) -> + withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f a3y a2y a1y) -> + maybe False id $ do + Refl <- testEquality sa3x sa3y + Refl <- testEquality sa2x sa2y + Refl <- testEquality sa1x sa1y + case dict3 sa3x sa2x sa1x :: Dict (Eq (f a3x a2x a1x)) of + Dict -> Just (x == y) + +instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) + . ( SDecide k4 + , SDecide k3 + , SDecide k2 + , SDecide k1 + , Dict4 Eq f + ) => Eq (Exinst.Some4 f) + where + {-# INLINABLE (==) #-} + (==) = \som4x som4y -> + withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f a4x a3x a2x a1x) -> + withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f a4y a3y a2y a1y) -> + maybe False id $ do + Refl <- testEquality sa4x sa4y + Refl <- testEquality sa3x sa3y + Refl <- testEquality sa2x sa2y + Refl <- testEquality sa1x sa1y + case dict4 sa4x sa3x sa2x sa1x :: Dict (Eq (f a4x a3x a2x a1x)) of + Dict -> Just (x == y) + +-------------------------------------------------------------------------------- +-- Ord + +instance forall (f :: k1 -> Type) + . ( SingKind k1 + , SDecide k1 + , Ord (Demote k1) + , Dict1 Ord f + , Eq (Exinst.Some1 f) + ) => Ord (Exinst.Some1 f) + where + {-# INLINABLE compare #-} + compare = \som1x som1y -> + withSome1Sing som1x $ \sa1x (x :: f a1x) -> + withSome1Sing som1y $ \sa1y (y :: f a1y) -> + let termCompare = compare (fromSing sa1x) (fromSing sa1y) + in maybe termCompare id $ do + Refl <- testEquality sa1x sa1y + case dict1 sa1x :: Dict (Ord (f a1x)) of + Dict -> Just (compare x y) + +instance forall (f :: k2 -> k1 -> Type) + . ( SingKind k2 + , SingKind k1 + , SDecide k2 + , SDecide k1 + , Ord (Demote k2) + , Ord (Demote k1) + , Dict2 Ord f + , Eq (Exinst.Some2 f) + ) => Ord (Exinst.Some2 f) + where + {-# INLINABLE compare #-} + compare = \som2x som2y -> + withSome2Sing som2x $ \sa2x sa1x (x :: f a2x a1x) -> + withSome2Sing som2y $ \sa2y sa1y (y :: f a2y a1y) -> + let termCompare = compare (fromSing sa2x, fromSing sa1x) + (fromSing sa2y, fromSing sa1y) + in maybe termCompare id $ do + Refl <- testEquality sa2x sa2y + Refl <- testEquality sa1x sa1y + case dict2 sa2x sa1x :: Dict (Ord (f a2x a1x)) of + Dict -> Just (compare x y) + +instance forall (f :: k3 -> k2 -> k1 -> Type) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , SDecide k3 + , SDecide k2 + , SDecide k1 + , Ord (Demote k3) + , Ord (Demote k2) + , Ord (Demote k1) + , Dict3 Ord f + , Eq (Exinst.Some3 f) + ) => Ord (Exinst.Some3 f) + where + {-# INLINABLE compare #-} + compare = \som3x som3y -> + withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f a3x a2x a1x) -> + withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f a3y a2y a1y) -> + let termCompare = compare + (fromSing sa3x, fromSing sa2x, fromSing sa1x) + (fromSing sa3y, fromSing sa2y, fromSing sa1y) + in maybe termCompare id $ do + Refl <- testEquality sa3x sa3y + Refl <- testEquality sa2x sa2y + Refl <- testEquality sa1x sa1y + case dict3 sa3x sa2x sa1x :: Dict (Ord (f a3x a2x a1x)) of + Dict -> Just (compare x y) + +instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , SDecide k4 + , SDecide k3 + , SDecide k2 + , SDecide k1 + , Ord (Demote k4) + , Ord (Demote k3) + , Ord (Demote k2) + , Ord (Demote k1) + , Dict4 Ord f + , Eq (Exinst.Some4 f) + ) => Ord (Exinst.Some4 f) + where + {-# INLINABLE compare #-} + compare = \som4x som4y -> + withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f a4x a3x a2x a1x) -> + withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f a4y a3y a2y a1y) -> + let termCompare = compare + (fromSing sa4x, fromSing sa3x, fromSing sa2x, fromSing sa1x) + (fromSing sa4y, fromSing sa3y, fromSing sa2y, fromSing sa1y) + in maybe termCompare id $ do + Refl <- testEquality sa4x sa4y + Refl <- testEquality sa3x sa3y + Refl <- testEquality sa2x sa2y + Refl <- testEquality sa1x sa1y + case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f a4x a3x a2x a1x)) of + Dict -> Just (compare x y) + +-------------------------------------------------------------------------------- +-- Generic + +type Eithers1 (f :: k1 -> Type) = + Eithers1' (EnumFromTo (MinBound :: k1) (MaxBound :: k1)) f + +-- | TODO: Mak1e this logarithmic. +type family Eithers1' (xs :: [k1]) (f :: k1 -> Type) :: Type where + Eithers1' (x ': '[]) f = f x + Eithers1' (x ': xs) f = Either (f x) (Eithers1' xs f) + +instance forall k1 (f :: k1 -> Type) + . ( SingKind k1 + , PEnum (Demote k1) + , PBounded (Demote k1) + , G.Generic (Demote k1) + , Dict1 G.Generic f + , Dict1 (Inj (Eithers1 f)) f + ) => G.Generic (Exinst.Some1 f) + where + type Rep (Exinst.Some1 (f :: k1 -> Type)) = + G.Rep (Demote k1, Eithers1 f) + {-# INLINABLE from #-} + from = \s1x -> withSome1Sing s1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (G.Generic (f a1)) of + Dict -> case dict1 sa1 :: Dict (Inj (Eithers1 f) (f a1)) of + Dict -> G.from (fromSing sa1, inj x) + {-# INLINABLE to #-} + to = \(G.M1 (G.M1 (G.M1 (G.K1 da1) G.:*: G.M1 (G.K1 ex)))) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (Inj (Eithers1 f) (f a1)) of + Dict -> case prj ex of + Just x -> Exinst.Some1 sa1 (x :: f a1) + Nothing -> error "Generic Some1: Malformed Rep" + +--- +type Eithers2 (f :: k2 -> k1 -> Type) = + Eithers2' (Cartesian2 (EnumFromTo (MinBound :: k2) (MaxBound :: k2)) + (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f + +-- | TODO: Mak1e this logarithmic. +type family Eithers2' (xs :: [(k2, k1)]) (f :: k2 -> k1 -> Type) :: Type where + Eithers2' ( '(x2, x1) ': '[]) f = f x2 x1 + Eithers2' ( '(x2, x1) ': xs) f = Either (f x2 x1) (Eithers2' xs f) + +type family Cartesian2 (xs2 :: [k2]) (xs1 :: [k1]) :: [(k2,k1)] where + Cartesian2 '[] xs1 = '[] + Cartesian2 (x2 ': xs2) xs1 = + List.Concat [List.Map (Tuple2Sym1 x2) xs1, Cartesian2 xs2 xs1] + + +instance forall k2 k1 (f :: k2 -> k1 -> Type) + . ( SingKind k2 + , SingKind k1 + , PEnum (Demote k2) + , PEnum (Demote k1) + , PBounded (Demote k2) + , PBounded (Demote k1) + , G.Generic (Demote k2) + , G.Generic (Demote k1) + , Dict2 G.Generic f + , Dict2 (Inj (Eithers2 f)) f + ) => G.Generic (Exinst.Some2 f) + where + type Rep (Exinst.Some2 (f :: k2 -> k1 -> Type)) = + G.Rep ((Demote k2, Demote k1), Eithers2 f) + {-# INLINABLE from #-} + from = \s2x -> withSome2Sing s2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (G.Generic (f a2 a1)) of + Dict -> case dict2 sa2 sa1 :: Dict (Inj (Eithers2 f) (f a2 a1)) of + Dict -> G.from ((fromSing sa2, fromSing sa1), inj x) + {-# INLINABLE to #-} + to = \(G.M1 (G.M1 (G.M1 (G.K1 (da2, da1)) G.:*: G.M1 (G.K1 ex)))) -> + withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict2 sa2 sa1 :: Dict (Inj (Eithers2 f) (f a2 a1)) of + Dict -> case prj ex of + Just x -> Exinst.Some2 sa2 sa1 (x :: f a2 a1) + Nothing -> error "Generic Some2: Malformed Rep" + + +--- +type Eithers3 (f :: k3 -> k2 -> k1 -> Type) = + Eithers3' (Cartesian3 (EnumFromTo (MinBound :: k3) (MaxBound :: k3)) + (EnumFromTo (MinBound :: k2) (MaxBound :: k2)) + (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f + +-- | TODO: Mak1e this logarithmic. +type family Eithers3' (xs :: [(k3, (k2, k1))]) (f :: k3 -> k2 -> k1 -> Type) :: Type where + Eithers3' ( '(x3, '(x2, x1)) ': '[]) f = f x3 x2 x1 + Eithers3' ( '(x3, '(x2, x1)) ': xs) f = Either (f x3 x2 x1) (Eithers3' xs f) + +-- | We use nested 2-tuples instead of 3-tuples because it's easier to implement. +type family Cartesian3 (xs3 :: [k3]) (xs2 :: [k2]) (xs1 :: [k1]) :: [(k3,(k2,k1))] where + Cartesian3 '[] xs2 xs1 = '[] + Cartesian3 (x3 ': xs3) xs2 xs1 = + List.Concat [ List.Map (Tuple2Sym1 x3) (Cartesian2 xs2 xs1) + , Cartesian3 xs3 xs2 xs1 ] + + +instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , PEnum (Demote k3) + , PEnum (Demote k2) + , PEnum (Demote k1) + , PBounded (Demote k3) + , PBounded (Demote k2) + , PBounded (Demote k1) + , G.Generic (Demote k3) + , G.Generic (Demote k2) + , G.Generic (Demote k1) + , Dict3 G.Generic f + , Dict3 (Inj (Eithers3 f)) f + ) => G.Generic (Exinst.Some3 f) + where + type Rep (Exinst.Some3 (f :: k3 -> k2 -> k1 -> Type)) = + G.Rep ((Demote k3, Demote k2, Demote k1), Eithers3 f) + {-# INLINABLE from #-} + from = \s3x -> withSome3Sing s3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (G.Generic (f a3 a2 a1)) of + Dict -> case dict3 sa3 sa2 sa1 :: Dict (Inj (Eithers3 f) (f a3 a2 a1)) of + Dict -> G.from ((fromSing sa3, fromSing sa2, fromSing sa1), inj x) + {-# INLINABLE to #-} + to = \(G.M1 (G.M1 (G.M1 (G.K1 (da3, da2, da1)) G.:*: G.M1 (G.K1 ex)))) -> + withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict3 sa3 sa2 sa1 :: Dict (Inj (Eithers3 f) (f a3 a2 a1)) of + Dict -> case prj ex of + Just x -> Exinst.Some3 sa3 sa2 sa1 (x :: f a3 a2 a1) + Nothing -> error "Generic Some3: Malformed Rep" + + +--- +type Eithers4 (f :: k4 -> k3 -> k2 -> k1 -> Type) = + Eithers4' (Cartesian4 (EnumFromTo (MinBound :: k4) (MaxBound :: k4)) + (EnumFromTo (MinBound :: k3) (MaxBound :: k3)) + (EnumFromTo (MinBound :: k2) (MaxBound :: k2)) + (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f + +-- | TODO: Mak1e this logarithmic. +type family Eithers4' (xs :: [(k4, (k3, (k2, k1)))]) (f :: k4 -> k3 -> k2 -> k1 -> Type) :: Type where + Eithers4' ( '( x4, '(x3, '(x2, x1))) ': '[]) f = f x4 x3 x2 x1 + Eithers4' ( '( x4, '(x3, '(x2, x1))) ': xs) f = Either (f x4 x3 x2 x1) (Eithers4' xs f) + +-- | We use nested 2-tuples instead of 4-tuples because it's easier to implement. +type family Cartesian4 (xs4 :: [k4]) (xs3 :: [k3]) (xs2 :: [k2]) (xs1 :: [k1]) :: [(k4,(k3,(k2,k1)))] where + Cartesian4 '[] xs3 xs2 xs1 = '[] + Cartesian4 (x4 ': xs4) xs3 xs2 xs1 = + List.Concat [ List.Map (Tuple2Sym1 x4) (Cartesian3 xs3 xs2 xs1) + , Cartesian4 xs4 xs3 xs2 xs1 ] + + +instance forall k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , PEnum (Demote k4) + , PEnum (Demote k3) + , PEnum (Demote k2) + , PEnum (Demote k1) + , PBounded (Demote k4) + , PBounded (Demote k3) + , PBounded (Demote k2) + , PBounded (Demote k1) + , G.Generic (Demote k4) + , G.Generic (Demote k3) + , G.Generic (Demote k2) + , G.Generic (Demote k1) + , Dict4 G.Generic f + , Dict4 (Inj (Eithers4 f)) f + ) => G.Generic (Exinst.Some4 f) + where + type Rep (Exinst.Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type)) = + G.Rep ((Demote k4, Demote k3, Demote k2, Demote k1), Eithers4 f) + {-# INLINABLE from #-} + from = \s4x -> withSome4Sing s4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (G.Generic (f a4 a3 a2 a1)) of + Dict -> case dict4 sa4 sa3 sa2 sa1 :: Dict (Inj (Eithers4 f) (f a4 a3 a2 a1)) of + Dict -> G.from ((fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1), inj x) + {-# INLINABLE to #-} + to = \(G.M1 (G.M1 (G.M1 (G.K1 (da4, da3, da2, da1)) G.:*: G.M1 (G.K1 ex)))) -> + withSomeSing da4 $ \(sa4 :: Sing (a4 :: k4)) -> + withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Inj (Eithers4 f) (f a4 a3 a2 a1)) of + Dict -> case prj ex of + Just x -> Exinst.Some4 sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) + Nothing -> error "Generic Some4: Malformed Rep" + +-------------------------------------------------------------------------------- +-------------------------------------------------------------------------------- +-- Out of the box 'DictX' instances for some @base@ types + +instance + (c 'False, c 'True + ) => Dict0 (c :: Bool -> Constraint) where + {-# INLINABLE dict0 #-} + dict0 = \case { SFalse -> Dict; STrue -> Dict } + +instance + ( c (f 'False), c (f 'True) + ) => Dict1 c (f :: Bool -> k0) where + {-# INLINABLE dict1 #-} + dict1 = \case { SFalse -> Dict; STrue -> Dict } + +instance + ( Dict1 c (f 'False), Dict1 c (f 'True) + ) => Dict2 c (f :: Bool -> k1 -> k0) where + {-# INLINABLE dict2 #-} + dict2 = \x -> case x of { SFalse -> dict1; STrue -> dict1 } + +instance + ( Dict2 c (f 'False), Dict2 c (f 'True) + ) => Dict3 c (f :: Bool -> k2 -> k1 -> k0) where + {-# INLINABLE dict3 #-} + dict3 = \x -> case x of { SFalse -> dict2; STrue -> dict2 } + +instance + ( Dict3 c (f 'False), Dict3 c (f 'True) + ) => Dict4 c (f :: Bool -> k3 -> k2 -> k1 -> k0) where + {-# INLINABLE dict4 #-} + dict4 = \x -> case x of { SFalse -> dict3; STrue -> dict3 } + +-------------------------------------------------------------------------------- +-------------------------------------------------------------------------------- +-- Misc + +class Inj b a where + inj :: a -> b + prj :: b -> Maybe a +instance Inj a a where + {-# INLINE inj #-} + inj = id + {-# INLINE prj #-} + prj = Just +instance Inj (Either a b) a where + {-# INLINE inj #-} + inj = Left + {-# INLINE prj #-} + prj = either Just (const Nothing) +-- | TODO: Make this logarithmic. +instance {-# OVERLAPPABLE #-} Inj x a => Inj (Either b x) a where + {-# INLINE inj #-} + inj = Right . inj + {-# INLINE prj #-} + prj = either (const Nothing) prj + diff --git a/lib/Exinst/Instances/Binary.hs b/lib/Exinst/Instances/Binary.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Instances/Binary.hs @@ -0,0 +1,137 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'Bin.Binary' instances for 'Some1', 'Some2', 'Some3' +-- and 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', +-- 'Dict3' and 'Dict4' instances are available. +-- +-- See the README file in the @exinst@ package for more general documentation: +-- https://hackage.haskell.org/package/exinst#readme +module Exinst.Instances.Binary () where + +import qualified Data.Binary as Bin +import Data.Constraint +import Data.Singletons +import Prelude + +import Exinst.Internal + +-------------------------------------------------------------------------------- + +-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and +-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the +-- fully applied @f@ instances are compatible as well. +instance forall (f :: k1 -> *). + ( SingKind k1 + , Bin.Binary (Demote k1) + , Dict1 Bin.Binary f + ) => Bin.Binary (Some1 f) where + {-# INLINABLE put #-} + put = \some1x -> + withSome1Sing some1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (Bin.Binary (f a1)) of + Dict -> do + Bin.put (fromSing sa1) + Bin.put x + {-# INLINABLE get #-} + get = do + rsa1 <- Bin.get + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (Bin.Binary (f a1)) of + Dict -> do + x :: f a1 <- Bin.get + pure (Some1 sa1 x) + +-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and +-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the +-- fully applied @f@ instances are compatible as well. +instance forall (f :: k2 -> k1 -> *). + ( SingKind k2 + , SingKind k1 + , Bin.Binary (Demote k2) + , Bin.Binary (Demote k1) + , Dict2 Bin.Binary f + ) => Bin.Binary (Some2 f) where + {-# INLINABLE put #-} + put = \some2x -> + withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of + Dict -> do + Bin.put (fromSing sa2, fromSing sa1) + Bin.put x + {-# INLINABLE get #-} + get = do + (rsa2, rsa1) <- Bin.get + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of + Dict -> do + x :: f a2 a1 <- Bin.get + pure (Some2 sa2 sa1 x) + +-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and +-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the +-- fully applied @f@ instances are compatible as well. +instance forall (f :: k3 -> k2 -> k1 -> *). + ( SingKind k3 + , SingKind k2 + , SingKind k1 + , Bin.Binary (Demote k3) + , Bin.Binary (Demote k2) + , Bin.Binary (Demote k1) + , Dict3 Bin.Binary f + ) => Bin.Binary (Some3 f) where + {-# INLINABLE put #-} + put = \some3x -> + withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of + Dict -> do + Bin.put (fromSing sa3, fromSing sa2, fromSing sa1) + Bin.put x + {-# INLINABLE get #-} + get = do + (rsa3, rsa2, rsa1) <- Bin.get + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of + Dict -> do + x :: f a3 a2 a1 <- Bin.get + pure (Some3 sa3 sa2 sa1 x) + +-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and +-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the +-- fully applied @f@ instances are compatible as well. +instance forall (f :: k4 -> k3 -> k2 -> k1 -> *). + ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , Bin.Binary (Demote k4) + , Bin.Binary (Demote k3) + , Bin.Binary (Demote k2) + , Bin.Binary (Demote k1) + , Dict4 Bin.Binary f + ) => Bin.Binary (Some4 f) where + {-# INLINABLE put #-} + put = \some4x -> + withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Bin.Binary (f a4 a3 a2 a1)) of + Dict -> do + Bin.put (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1) + Bin.put x + {-# INLINABLE get #-} + get = do + (rsa4, rsa3, rsa2, rsa1) <- Bin.get + withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Bin.Binary (f a4 a3 a2 a1)) of + Dict -> do + x :: f a4 a3 a2 a1 <- Bin.get + pure (Some4 sa4 sa3 sa2 sa1 x) diff --git a/lib/Exinst/Instances/Bytes.hs b/lib/Exinst/Instances/Bytes.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Instances/Bytes.hs @@ -0,0 +1,138 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'By.Serial' instances for 'Some1', 'Some2', 'Some3' +-- and 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', +-- 'Dict3' and 'Dict4' instances are available. +-- +-- See the README file in the @exinst@ package for more general documentation: +-- https://hackage.haskell.org/package/exinst#readme +module Exinst.Instances.Bytes () where + +import qualified Data.Bytes.Serial as By +import Data.Constraint +import Data.Singletons +import Prelude + +import Exinst.Internal + +-------------------------------------------------------------------------------- + +-- | Compatible with the 'Data.Binary.Binary' instance and +-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the +-- fully applied @f@ instances are compatible as well. +instance forall (f :: k1 -> *). + ( SingKind k1 + , By.Serial (Demote k1) + , Dict1 By.Serial f + ) => By.Serial (Some1 f) where + {-# INLINABLE serialize #-} + serialize = \some1x -> + withSome1Sing some1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (By.Serial (f a1)) of + Dict -> do + By.serialize (fromSing sa1) + By.serialize x + {-# INLINABLE deserialize #-} + deserialize = do + rsa1 <- By.deserialize + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (By.Serial (f a1)) of + Dict -> do + x :: f a1 <- By.deserialize + pure (Some1 sa1 x) + +-- | Compatible with the 'Data.Binary.Binary' instance and +-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the +-- fully applied @f@ instances are compatible as well. +instance forall (f :: k2 -> k1 -> *). + ( SingKind k2 + , SingKind k1 + , By.Serial (Demote k2) + , By.Serial (Demote k1) + , Dict2 By.Serial f + ) => By.Serial (Some2 f) where + {-# INLINABLE serialize #-} + serialize = \some2x -> + withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (By.Serial (f a2 a1)) of + Dict -> do + By.serialize (fromSing sa2, fromSing sa1) + By.serialize x + {-# INLINABLE deserialize #-} + deserialize = do + (rsa2, rsa1) <- By.deserialize + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict2 sa2 sa1 :: Dict (By.Serial (f a2 a1)) of + Dict -> do + x :: f a2 a1 <- By.deserialize + pure (Some2 sa2 sa1 x) + +-- | Compatible with the 'Data.Binary.Binary' instance and +-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the +-- fully applied @f@ instances are compatible as well. +instance forall (f :: k3 -> k2 -> k1 -> *). + ( SingKind k3 + , SingKind k2 + , SingKind k1 + , By.Serial (Demote k3) + , By.Serial (Demote k2) + , By.Serial (Demote k1) + , Dict3 By.Serial f + ) => By.Serial (Some3 f) where + {-# INLINABLE serialize #-} + serialize = \some3x -> + withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f a3 a2 a1)) of + Dict -> do + By.serialize (fromSing sa3, fromSing sa2, fromSing sa1) + By.serialize x + {-# INLINABLE deserialize #-} + deserialize = do + (rsa3, rsa2, rsa1) <- By.deserialize + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f a3 a2 a1)) of + Dict -> do + x :: f a3 a2 a1 <- By.deserialize + pure (Some3 sa3 sa2 sa1 x) + +-- | Compatible with the 'Data.Binary.Binary' instance and +-- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the +-- fully applied @f@ instances are compatible as well. +instance forall (f :: k4 -> k3 -> k2 -> k1 -> *). + ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , By.Serial (Demote k4) + , By.Serial (Demote k3) + , By.Serial (Demote k2) + , By.Serial (Demote k1) + , Dict4 By.Serial f + ) => By.Serial (Some4 f) where + {-# INLINABLE serialize #-} + serialize = \some4x -> + withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f a4 a3 a2 a1)) of + Dict -> do + By.serialize (fromSing sa4, fromSing sa3, + fromSing sa2, fromSing sa1) + By.serialize x + {-# INLINABLE deserialize #-} + deserialize = do + (rsa4, rsa3, rsa2, rsa1) <- By.deserialize + withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f a4 a3 a2 a1)) of + Dict -> do + x :: f a4 a3 a2 a1 <- By.deserialize + pure (Some4 sa4 sa3 sa2 sa1 x) diff --git a/lib/Exinst/Instances/Cereal.hs b/lib/Exinst/Instances/Cereal.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Instances/Cereal.hs @@ -0,0 +1,138 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'Cer.Serialize' instances for 'Some1', 'Some2', 'Some3' +-- and 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', +-- 'Dict3' and 'Dict4' instances are available. +-- +-- See the README file in the @exinst@ package for more general documentation: +-- https://hackage.haskell.org/package/exinst#readme +module Exinst.Instances.Cereal () where + +import qualified Data.Serialize as Cer +import Data.Constraint +import Data.Singletons +import Prelude + +import Exinst.Internal + +-------------------------------------------------------------------------------- + +-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and +-- 'Data.Binary.Binary' instance, provided all of the 'Demote's and the fully +-- applied @f@ instances are compatible as well. +instance forall (f :: k1 -> *). + ( SingKind k1 + , Cer.Serialize (Demote k1) + , Dict1 Cer.Serialize f + ) => Cer.Serialize (Some1 f) where + {-# INLINABLE put #-} + put = \some1x -> + withSome1Sing some1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (Cer.Serialize (f a1)) of + Dict -> do + Cer.put (fromSing sa1) + Cer.put x + {-# INLINABLE get #-} + get = do + rsa1 <- Cer.get + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (Cer.Serialize (f a1)) of + Dict -> do + x :: f a1 <- Cer.get + pure (Some1 sa1 x) + +-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and +-- 'Data.Binary.Binary' instance, provided all of the 'Demote's and the fully +-- applied @f@ instances are compatible as well. +instance forall (f :: k2 -> k1 -> *). + ( SingKind k2 + , SingKind k1 + , Cer.Serialize (Demote k2) + , Cer.Serialize (Demote k1) + , Dict2 Cer.Serialize f + ) => Cer.Serialize (Some2 f) where + {-# INLINABLE put #-} + put = \some2x -> + withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (Cer.Serialize (f a2 a1)) of + Dict -> do + Cer.put (fromSing sa2, fromSing sa1) + Cer.put x + {-# INLINABLE get #-} + get = do + (rsa2, rsa1) <- Cer.get + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict2 sa2 sa1 :: Dict (Cer.Serialize (f a2 a1)) of + Dict -> do + x :: f a2 a1 <- Cer.get + pure (Some2 sa2 sa1 x) + +-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and +-- 'Data.Binary.Binary' instance, provided all of the 'Demote's and the fully +-- applied @f@ instances are compatible as well. +instance forall (f :: k3 -> k2 -> k1 -> *). + ( SingKind k3 + , SingKind k2 + , SingKind k1 + , Cer.Serialize (Demote k3) + , Cer.Serialize (Demote k2) + , Cer.Serialize (Demote k1) + , Dict3 Cer.Serialize f + ) => Cer.Serialize (Some3 f) where + {-# INLINABLE put #-} + put = \some3x -> + withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a3 a2 a1)) of + Dict -> do + Cer.put (fromSing sa3, fromSing sa2, fromSing sa1) + Cer.put x + {-# INLINABLE get #-} + get = do + (rsa3, rsa2, rsa1) <- Cer.get + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict3 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a3 a2 a1)) of + Dict -> do + x :: f a3 a2 a1 <- Cer.get + pure (Some3 sa3 sa2 sa1 x) + +-- | Compatible with the 'Data.Bytes.Serial.Serial' instance and +-- 'Data.Binary.Binary' instance, provided all of the 'Demote's and the fully +-- applied @f@ instances are compatible as well. +instance forall (f :: k4 -> k3 -> k2 -> k1 -> *). + ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , Cer.Serialize (Demote k4) + , Cer.Serialize (Demote k3) + , Cer.Serialize (Demote k2) + , Cer.Serialize (Demote k1) + , Dict4 Cer.Serialize f + ) => Cer.Serialize (Some4 f) where + {-# INLINABLE put #-} + put = \some4x -> + withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a4 a3 a2 a1)) of + Dict -> do + Cer.put (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1) + Cer.put x + {-# INLINABLE get #-} + get = do + (rsa4, rsa3, rsa2, rsa1) <- Cer.get + withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a4 a3 a2 a1)) of + Dict -> do + x :: f a4 a3 a2 a1 <- Cer.get + pure (Some4 sa4 sa3 sa2 sa1 x) + diff --git a/lib/Exinst/Instances/DeepSeq.hs b/lib/Exinst/Instances/DeepSeq.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Instances/DeepSeq.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'NFData' instances for 'Some1', 'Some2', 'Some3' and +-- 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', 'Dict3' +-- and 'Dict4' instances are available. +-- +-- See the README file in the @exinst@ package for more general documentation: +-- https://hackage.haskell.org/package/exinst#readme +module Exinst.Instances.DeepSeq () where + +import Control.DeepSeq (NFData(rnf)) +import Data.Constraint +import Prelude + +import Exinst.Internal + +-------------------------------------------------------------------------------- + +instance forall (f :: k1 -> *). + ( Dict1 NFData f + ) => NFData (Some1 f) where + {-# INLINABLE rnf #-} + rnf = \(!some1x) -> + withSome1Sing some1x $ \ !sa1 !(x :: f a1) -> + case dict1 sa1 :: Dict (NFData (f a1)) of + Dict -> rnf x `seq` () + +instance forall (f :: k2 -> k1 -> *). + ( Dict2 NFData f + ) => NFData (Some2 f) where + {-# INLINABLE rnf #-} + rnf = \(!some2x) -> + withSome2Sing some2x $ \ !sa2 !sa1 !(x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (NFData (f a2 a1)) of + Dict -> rnf x `seq` () + +instance forall (f :: k3 -> k2 -> k1 -> *). + ( Dict3 NFData f + ) => NFData (Some3 f) where + {-# INLINABLE rnf #-} + rnf = \(!some3x) -> + withSome3Sing some3x $ \ !sa3 !sa2 !sa1 !(x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (NFData (f a3 a2 a1)) of + Dict -> rnf x `seq` () + +instance forall (f :: k4 -> k3 -> k2 -> k1 -> *). + ( Dict4 NFData f + ) => NFData (Some4 f) where + {-# INLINABLE rnf #-} + rnf = \(!some4x) -> + withSome4Sing some4x $ \ !(sa4) !sa3 !sa2 !sa1 !(x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (NFData (f a4 a3 a2 a1)) of + Dict -> rnf x `seq` () + diff --git a/lib/Exinst/Instances/Hashable.hs b/lib/Exinst/Instances/Hashable.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Instances/Hashable.hs @@ -0,0 +1,99 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'Hashable' instances for 'Some1', 'Some2', 'Some3' and +-- 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', 'Dict3' +-- and 'Dict4' instances are available. +-- +-- See the README file in the @exinst@ package for more general documentation: +-- https://hackage.haskell.org/package/exinst#readme +module Exinst.Instances.Hashable () where + +import Data.Hashable (Hashable(hashWithSalt)) +import Data.Constraint +import Data.Singletons +import Prelude + +import Exinst.Internal + +-------------------------------------------------------------------------------- + +-- | Some salt we add to hashes calculated in this module. +salt0 :: Int +salt0 = 6700417 + +-------------------------------------------------------------------------------- + +instance forall (f :: k1 -> *) + . ( SingKind k1 + , Hashable (Demote k1) + , Dict1 Hashable f + ) => Hashable (Some1 f) + where + {-# INLINABLE hashWithSalt #-} + hashWithSalt salt some1x = withSome1Sing some1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (Hashable (f a1)) of + Dict -> salt `hashWithSalt` salt0 + `hashWithSalt` fromSing sa1 + `hashWithSalt` x + +instance forall (f :: k2 -> k1 -> *) + . ( SingKind k2 + , SingKind k1 + , Hashable (Demote k2) + , Hashable (Demote k1) + , Dict2 Hashable f + ) => Hashable (Some2 f) + where + {-# INLINABLE hashWithSalt #-} + hashWithSalt salt some2x = withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (Hashable (f a2 a1)) of + Dict -> salt `hashWithSalt` salt0 + `hashWithSalt` fromSing sa2 + `hashWithSalt` fromSing sa1 + `hashWithSalt` x + +instance forall (f :: k3 -> k2 -> k1 -> *) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , Hashable (Demote k3) + , Hashable (Demote k2) + , Hashable (Demote k1) + , Dict3 Hashable f + ) => Hashable (Some3 f) + where + {-# INLINABLE hashWithSalt #-} + hashWithSalt salt some3x = withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (Hashable (f a3 a2 a1)) of + Dict -> salt `hashWithSalt` salt0 + `hashWithSalt` fromSing sa3 + `hashWithSalt` fromSing sa2 + `hashWithSalt` fromSing sa1 + `hashWithSalt` x + +instance forall (f :: k4 -> k3 -> k2 -> k1 -> *) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , Hashable (Demote k4) + , Hashable (Demote k3) + , Hashable (Demote k2) + , Hashable (Demote k1) + , Dict4 Hashable f + ) => Hashable (Some4 f) + where + {-# INLINABLE hashWithSalt #-} + hashWithSalt salt some4x = withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Hashable (f a4 a3 a2 a1)) of + Dict -> salt `hashWithSalt` salt0 + `hashWithSalt` fromSing sa4 + `hashWithSalt` fromSing sa3 + `hashWithSalt` fromSing sa2 + `hashWithSalt` fromSing sa1 + `hashWithSalt` x diff --git a/lib/Exinst/Instances/QuickCheck.hs b/lib/Exinst/Instances/QuickCheck.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Instances/QuickCheck.hs @@ -0,0 +1,106 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeInType #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'QC.arbitrary' instances for 'Exinst.Some1', 'Some2', +-- 'Some3' and 'Some4' from "Exinst", provided situable 'Dict1', +-- 'Dict2', 'Dict3' and 'Dict4' instances are available. +-- +-- See the README file for more general documentation: https://hackage.haskell.org/package/exinst#readme +module Exinst.Instances.QuickCheck () where + +import Data.Constraint +import Data.Kind (Type) +import Data.Singletons (SingKind, Sing, Demote, withSomeSing) +import qualified Test.QuickCheck as QC + +import Exinst.Internal + +-------------------------------------------------------------------------------- + +instance + forall k1 (f :: k1 -> Type). + ( SingKind k1 + , QC.Arbitrary (Demote k1) + , Dict1 QC.Arbitrary f + ) => QC.Arbitrary (Some1 f) where + arbitrary = do + da1 <- QC.arbitrary + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (QC.Arbitrary (f a1)) of + Dict -> Some1 sa1 <$> QC.arbitrary + shrink = \s1x -> withSome1Sing s1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (QC.Arbitrary (f a1)) of + Dict -> Some1 sa1 <$> QC.shrink x + +instance + forall k2 k1 (f :: k2 -> k1 -> Type). + ( SingKind k2 + , SingKind k1 + , QC.Arbitrary (Demote k2) + , QC.Arbitrary (Demote k1) + , Dict2 QC.Arbitrary f + ) => QC.Arbitrary (Some2 f) where + arbitrary = do + da2 <- QC.arbitrary + da1 <- QC.arbitrary + withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict2 sa2 sa1 :: Dict (QC.Arbitrary (f a2 a1)) of + Dict -> Some2 sa2 sa1 <$> QC.arbitrary + shrink = \s2x -> withSome2Sing s2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (QC.Arbitrary (f a2 a1)) of + Dict -> Some2 sa2 sa1 <$> QC.shrink x + +instance + forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type). + ( SingKind k3 + , SingKind k2 + , SingKind k1 + , QC.Arbitrary (Demote k3) + , QC.Arbitrary (Demote k2) + , QC.Arbitrary (Demote k1) + , Dict3 QC.Arbitrary f + ) => QC.Arbitrary (Some3 f) where + arbitrary = do + da3 <- QC.arbitrary + da2 <- QC.arbitrary + da1 <- QC.arbitrary + withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict3 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a3 a2 a1)) of + Dict -> Some3 sa3 sa2 sa1 <$> QC.arbitrary + shrink = \s3x -> withSome3Sing s3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a3 a2 a1)) of + Dict -> Some3 sa3 sa2 sa1 <$> QC.shrink x + +instance + forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type). + ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , QC.Arbitrary (Demote k4) + , QC.Arbitrary (Demote k3) + , QC.Arbitrary (Demote k2) + , QC.Arbitrary (Demote k1) + , Dict4 QC.Arbitrary f + ) => QC.Arbitrary (Some4 f) where + arbitrary = do + da4 <- QC.arbitrary + da3 <- QC.arbitrary + da2 <- QC.arbitrary + da1 <- QC.arbitrary + withSomeSing da4 $ \(sa4 :: Sing (a4 :: k4)) -> + withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a4 a3 a2 a1)) of + Dict -> Some4 sa4 sa3 sa2 sa1 <$> QC.arbitrary + shrink = \s3x -> withSome4Sing s3x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a4 a3 a2 a1)) of + Dict -> Some4 sa4 sa3 sa2 sa1 <$> QC.shrink x + diff --git a/lib/Exinst/Instances/Serialise.hs b/lib/Exinst/Instances/Serialise.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Instances/Serialise.hs @@ -0,0 +1,125 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | This module exports 'Serialise' instances (which provide +-- binary serialisation via the CBOR format) for 'Some1', +-- 'Some2', 'Some3' and 'Some4' from "Exinst", provided situable +-- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available. +-- +-- See the README file in the @exinst@ package for more general documentation: +-- https://hackage.haskell.org/package/exinst#readme +module Exinst.Instances.Serialise () where + +import Codec.Serialise +import Codec.Serialise.Decoding (decodeListLenOf) +import Data.Constraint +import Data.Singletons +import Prelude + +import Exinst.Internal + +-------------------------------------------------------------------------------- + +instance forall (f :: k1 -> *) + . ( SingKind k1 + , Serialise (Demote k1) + , Dict1 Serialise f + ) => Serialise (Some1 f) + where + {-# INLINABLE encode #-} + encode = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) -> + case dict1 sa1 :: Dict (Serialise (f a1)) of + Dict -> encode (fromSing sa1, x) + {-# INLINABLE decode #-} + decode = do + decodeListLenOf 2 + rsa1 <- decode + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (Serialise (f a1)) of + Dict -> do + x :: f a1 <- decode + pure (Some1 sa1 x) + +instance forall (f :: k2 -> k1 -> *) + . ( SingKind k2 + , SingKind k1 + , Serialise (Demote k2) + , Serialise (Demote k1) + , Dict2 Serialise f + ) => Serialise (Some2 f) + where + {-# INLINABLE encode #-} + encode = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (Serialise (f a2 a1)) of + Dict -> encode (fromSing sa2, fromSing sa1, x) + + + {-# INLINABLE decode #-} + decode = do + decodeListLenOf 3 + rsa2 <- decode; rsa1 <- decode + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict2 sa2 sa1 :: Dict (Serialise (f a2 a1)) of + Dict -> do + x :: f a2 a1 <- decode + pure (Some2 sa2 sa1 x) + +instance forall (f :: k3 -> k2 -> k1 -> *) + . ( SingKind k3 + , SingKind k2 + , SingKind k1 + , Serialise (Demote k3) + , Serialise (Demote k2) + , Serialise (Demote k1) + , Dict3 Serialise f + ) => Serialise (Some3 f) + where + {-# INLINABLE encode #-} + encode = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> + case dict3 sa3 sa2 sa1 :: Dict (Serialise (f a3 a2 a1)) of + Dict -> encode (fromSing sa3, fromSing sa2, fromSing sa1, x) + {-# INLINABLE decode #-} + decode = do + decodeListLenOf 4 + rsa3 <- decode; rsa2 <- decode; rsa1 <- decode + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict3 sa3 sa2 sa1 :: Dict (Serialise (f a3 a2 a1)) of + Dict -> do + x :: f a3 a2 a1 <- decode + pure (Some3 sa3 sa2 sa1 x) + +instance forall (f :: k4 -> k3 -> k2 -> k1 -> *) + . ( SingKind k4 + , SingKind k3 + , SingKind k2 + , SingKind k1 + , Serialise (Demote k4) + , Serialise (Demote k3) + , Serialise (Demote k2) + , Serialise (Demote k1) + , Dict4 Serialise f + ) => Serialise (Some4 f) + where + {-# INLINABLE encode #-} + encode = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Serialise (f a4 a3 a2 a1)) of + Dict -> encode (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1, x) + {-# INLINABLE decode #-} + decode = do + decodeListLenOf 5 + rsa4 <- decode; rsa3 <- decode; rsa2 <- decode; rsa1 <- decode; + withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> + withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> + withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict4 sa4 sa3 sa2 sa1 :: Dict (Serialise (f a4 a3 a2 a1)) of + Dict -> do + x :: f a4 a3 a2 a1 <- decode + pure (Some4 sa4 sa3 sa2 sa1 x) diff --git a/lib/Exinst/Internal.hs b/lib/Exinst/Internal.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Internal.hs @@ -0,0 +1,443 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} + + +module Exinst.Internal + ( -- * 1 type index + Some1(Some1) + , some1 + , fromSome1 + , _Some1 + , withSome1 + , withSome1Sing + , some1SingRep + , same1 + , Dict1(dict1) + + -- * 2 type indexes + , Some2(Some2) + , some2 + , fromSome2 + , _Some2 + , withSome2 + , withSome2Sing + , some2SingRep + , same2 + , Dict2(dict2) + + -- * 3 type indexes + , Some3(Some3) + , some3 + , fromSome3 + , _Some3 + , withSome3 + , withSome3Sing + , some3SingRep + , same3 + , Dict3(dict3) + + -- * 4 type indexes + , Some4(Some4) + , some4 + , fromSome4 + , _Some4 + , withSome4 + , withSome4Sing + , some4SingRep + , same4 + , Dict4(dict4) + + -- * Miscellaneous + , Dict0(dict0) + ) where + +import Data.Constraint +import Data.Kind (Type) +import Data.Profunctor (dimap, Choice(right')) +import Data.Singletons +import Data.Singletons.Decide +import Data.Type.Equality +import Prelude + +-------------------------------------------------------------------------------- + +data Some1 (f1 :: k1 -> Type) = forall a1. + Some1 !(Sing a1) !(f1 a1) + +data Some2 (f2 :: k2 -> k1 -> Type) = forall a2 a1. + Some2 !(Sing a2) !(Sing a1) !(f2 a2 a1) + +data Some3 (f3 :: k3 -> k2 -> k1 -> Type) = forall a3 a2 a1. + Some3 !(Sing a3) !(Sing a2) !(Sing a1) !(f3 a3 a2 a1) + +data Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) = forall a4 a3 a2 a1. + Some4 !(Sing a4) !(Sing a3) !(Sing a2) !(Sing a1) !(f4 a4 a3 a2 a1) + +-------------------------------------------------------------------------------- + +some1 + :: forall (f1 :: k1 -> Type) a1 + . SingI a1 + => f1 a1 + -> Some1 f1 -- ^ +some1 = Some1 (sing :: Sing a1) +{-# INLINE some1 #-} + +some2 + :: forall (f2 :: k2 -> k1 -> Type) a2 a1 + . (SingI a2, SingI a1) + => f2 a2 a1 + -> Some2 f2 -- ^ +some2 = Some2 (sing :: Sing a2) (sing :: Sing a1) +{-# INLINE some2 #-} + +some3 + :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1 + . (SingI a3, SingI a2, SingI a1) + => f3 a3 a2 a1 + -> Some3 f3 -- ^ +some3 = Some3 (sing :: Sing a3) (sing :: Sing a2) (sing :: Sing a1) +{-# INLINE some3 #-} + +some4 + :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1 + . (SingI a4, SingI a3, SingI a2, SingI a1) + => f4 a4 a3 a2 a1 + -> Some4 f4 -- ^ +some4 = Some4 (sing :: Sing a4) (sing :: Sing a3) + (sing :: Sing a2) (sing :: Sing a1) +{-# INLINE some4 #-} + +-------------------------------------------------------------------------------- + +withSome1 + :: forall (f1 :: k1 -> Type) (r :: Type) + . Some1 f1 + -> (forall a1. SingI a1 => f1 a1 -> r) + -> r -- ^ +withSome1 s1 g = withSome1Sing s1 (\_ -> g) +{-# INLINABLE withSome1 #-} + +withSome2 + :: forall (f2 :: k2 -> k1 -> Type) (r :: Type) + . Some2 f2 + -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r) + -> r -- ^ +withSome2 s2 g = withSome2Sing s2 (\_ _ -> g) +{-# INLINABLE withSome2 #-} + +withSome3 + :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type) + . Some3 f3 + -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r) + -> r -- ^ +withSome3 s3 g = withSome3Sing s3 (\_ _ _ -> g) +{-# INLINABLE withSome3 #-} + +withSome4 + :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type) + . Some4 f4 + -> (forall a4 a3 a2 a1 + . (SingI a4, SingI a3, SingI a2, SingI a1) + => f4 a4 a3 a2 a1 -> r) + -> r -- ^ +withSome4 s4 g = withSome4Sing s4 (\_ _ _ _ -> g) +{-# INLINABLE withSome4 #-} + +-------------------------------------------------------------------------------- + +-- | Like 'withSome1', but takes an explicit 'Sing' besides the 'SingI' instance. +withSome1Sing + :: forall (f1 :: k1 -> Type) (r :: Type) + . Some1 f1 + -> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r) + -> r -- ^ +withSome1Sing (Some1 sa1 x) g = withSingI sa1 (g sa1 x) +{-# INLINABLE withSome1Sing #-} + +-- | Like 'withSome2', but takes explicit 'Sing's besides the 'SingI' instances. +withSome2Sing + :: forall (f2 :: k2 -> k1 -> Type) (r :: Type) + . Some2 f2 + -> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r) + -> r -- ^ +withSome2Sing (Some2 sa2 sa1 x) g = withSingI sa2 (withSingI sa1 (g sa2 sa1 x)) +{-# INLINABLE withSome2Sing #-} + +-- | Like 'withSome3', but takes explicit 'Sing's besides the 'SingI' instances. +withSome3Sing + :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type) + . Some3 f3 + -> (forall a3 a2 a1 + . (SingI a3, SingI a2, SingI a1) + => Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r) + -> r -- ^ +withSome3Sing (Some3 sa3 sa2 sa1 x) g = + withSingI sa3 (withSingI sa2 (withSingI sa1 (g sa3 sa2 sa1 x))) +{-# INLINABLE withSome3Sing #-} + +-- | Like 'withSome4', but takes explicit 'Sing's besides the 'SingI' instances. +withSome4Sing + :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type) + . Some4 f4 + -> (forall a4 a3 a2 a1 + . (SingI a4, SingI a3, SingI a2, SingI a1) + => Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r) + -> r -- ^ +withSome4Sing (Some4 sa4 sa3 sa2 sa1 x) g = + withSingI sa4 (withSingI sa3 (withSingI sa2 (withSingI sa1 + (g sa4 sa3 sa2 sa1 x)))) +{-# INLINABLE withSome4Sing #-} + +-------------------------------------------------------------------------------- + +fromSome1 + :: forall (f1 :: k1 -> Type) a1 + . (SingI a1, SDecide k1) + => Some1 f1 + -> Maybe (f1 a1) -- ^ +fromSome1 = \(Some1 sa1' x) -> do + Refl <- testEquality sa1' (sing :: Sing a1) + return x +{-# INLINABLE fromSome1 #-} + +fromSome2 + :: forall (f2 :: k2 -> k1 -> Type) a2 a1 + . ( SingI a2, SDecide k2 + , SingI a1, SDecide k1 ) + => Some2 f2 + -> Maybe (f2 a2 a1) -- ^ +fromSome2 = \(Some2 sa2' sa1' x) -> do + Refl <- testEquality sa2' (sing :: Sing a2) + Refl <- testEquality sa1' (sing :: Sing a1) + return x +{-# INLINABLE fromSome2 #-} + +fromSome3 + :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1 + . ( SingI a3, SDecide k3 + , SingI a2, SDecide k2 + , SingI a1, SDecide k1 ) + => Some3 f3 + -> Maybe (f3 a3 a2 a1) -- ^ +fromSome3 = \(Some3 sa3' sa2' sa1' x) -> do + Refl <- testEquality sa3' (sing :: Sing a3) + Refl <- testEquality sa2' (sing :: Sing a2) + Refl <- testEquality sa1' (sing :: Sing a1) + return x +{-# INLINABLE fromSome3 #-} + +fromSome4 + :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1 + . ( SingI a4, SDecide k4 + , SingI a3, SDecide k3 + , SingI a2, SDecide k2 + , SingI a1, SDecide k1 ) + => Some4 f4 + -> Maybe (f4 a4 a3 a2 a1) -- ^ +fromSome4 = \(Some4 sa4' sa3' sa2' sa1' x) -> do + Refl <- testEquality sa4' (sing :: Sing a4) + Refl <- testEquality sa3' (sing :: Sing a3) + Refl <- testEquality sa2' (sing :: Sing a2) + Refl <- testEquality sa1' (sing :: Sing a1) + return x +{-# INLINABLE fromSome4 #-} + +-------------------------------------------------------------------------------- + +-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some1'. +_Some1 + :: forall (f1 :: k1 -> Type) a1 + . (SingI a1, SDecide k1) + => Prism' (Some1 f1) (f1 a1) +_Some1 = prism' some1 fromSome1 +{-# INLINE _Some1 #-} + +-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some2'. +_Some2 + :: forall (f2 :: k2 -> k1 -> Type) a2 a1 + . ( SingI a2, SDecide k2 + , SingI a1, SDecide k1 ) + => Prism' (Some2 f2) (f2 a2 a1) +_Some2 = prism' some2 fromSome2 +{-# INLINE _Some2 #-} + +-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some3'. +_Some3 + :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1 + . ( SingI a3, SDecide k3 + , SingI a2, SDecide k2 + , SingI a1, SDecide k1 ) + => Prism' (Some3 f3) (f3 a3 a2 a1) +_Some3 = prism' some3 fromSome3 +{-# INLINE _Some3 #-} + +-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some4'. +_Some4 + :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1 + . ( SingI a4, SDecide k4 + , SingI a3, SDecide k3 + , SingI a2, SDecide k2 + , SingI a1, SDecide k1 ) + => Prism' (Some4 f4) (f4 a4 a3 a2 a1) +_Some4 = prism' some4 fromSome4 +{-# INLINE _Some4 #-} + +-------------------------------------------------------------------------------- + +some1SingRep + :: SingKind k1 + => Some1 (f1 :: k1 -> Type) + -> Demote k1 -- ^ +some1SingRep = \(Some1 sa1 _) -> fromSing sa1 +{-# INLINE some1SingRep #-} + +some2SingRep + :: (SingKind k2, SingKind k1) + => Some2 (f2 :: k2 -> k1 -> Type) + -> (Demote k2, Demote k1) -- ^ +some2SingRep = \(Some2 sa2 sa1 _) -> (fromSing sa2, fromSing sa1) +{-# INLINE some2SingRep #-} + +some3SingRep + :: (SingKind k3, SingKind k2, SingKind k1) + => Some3 (f3 :: k3 -> k2 -> k1 -> Type) + -> (Demote k3, Demote k2, Demote k1) -- ^ +some3SingRep = \(Some3 sa3 sa2 sa1 _) -> + (fromSing sa3, fromSing sa2, fromSing sa1) +{-# INLINE some3SingRep #-} + +some4SingRep + :: (SingKind k4, SingKind k3, SingKind k2, SingKind k1) + => Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) + -> (Demote k4, Demote k3, Demote k2, Demote k1) -- ^ +some4SingRep = \(Some4 sa4 sa3 sa2 sa1 _) -> + (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1) +{-# INLINE some4SingRep #-} + +-------------------------------------------------------------------------------- + +-- | @'same1' x a b@ applies @x@ to the contents of @a@ and @b@ if their type +-- indexes are equal. +-- +-- Hint: @'same1' ('some1' . 'Exinst.P1') :: 'Some1' f -> 'Some1' g -> 'Some1' ('Exinst.P1' f g)@ +{-# INLINABLE same1 #-} +same1 + :: SDecide k1 + => (forall a1. SingI a1 => f a1 -> g a1 -> x) + -> Some1 (f :: k1 -> Type) + -> Some1 (g :: k1 -> Type) + -> Maybe x -- ^ +same1 z = \s1f s1g -> + withSome1Sing s1f $ \sa1 f -> + withSome1Sing s1g $ \sa1' g -> do + Refl <- testEquality sa1 sa1' + pure (z f g) + +-- | @'same2' x a b@ applies @x@ to the contents of @a@ and @b@ if their type +-- indexes are equal. +-- +-- Hint: @'same2' ('some2' . 'Exinst.P2') :: 'Some2' f -> 'Some2' g -> 'Some2' ('Exinst.P2' f g)@ +{-# INLINABLE same2 #-} +same2 + :: (SDecide k2, SDecide k1) + => (forall a2 a1. SingI a1 => f a2 a1 -> g a2 a1 -> x) + -> Some2 (f :: k2 -> k1 -> Type) + -> Some2 (g :: k2 -> k1 -> Type) + -> Maybe x -- ^ +same2 z = \s2l s2g -> + withSome2Sing s2l $ \sa2 sa1 f -> + withSome2Sing s2g $ \sa2' sa1' g -> do + Refl <- testEquality sa2 sa2' + Refl <- testEquality sa1 sa1' + pure (z f g) + +-- | @'same3' x a b@ applies @x@ to the contents of @a@ and @b@ if their type +-- indexes are equal. +-- +-- Hint: @'same3' ('some3' . 'Exinst.P3') :: 'Some3' f -> 'Some3' g -> 'Some3' ('Exinst.P3' f g)@ +{-# INLINABLE same3 #-} +same3 + :: (SDecide k3, SDecide k2, SDecide k1) + => (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) + => f a3 a2 a1 -> g a3 a2 a1 -> x) + -> Some3 (f :: k3 -> k2 -> k1 -> Type) + -> Some3 (g :: k3 -> k2 -> k1 -> Type) + -> Maybe x -- ^ +same3 z = \s3l s3g -> + withSome3Sing s3l $ \sa3 sa2 sa1 f -> + withSome3Sing s3g $ \sa3' sa2' sa1' g -> do + Refl <- testEquality sa3 sa3' + Refl <- testEquality sa2 sa2' + Refl <- testEquality sa1 sa1' + pure (z f g) + +-- | @'same4' x a b@ applies @x@ to the contents of @a@ and @b@ if their type +-- indexes are equal. +-- +-- Hint: @'same4' ('some4' . 'Exinst.P4') :: 'Some4' f -> 'Some4' g -> 'Some4' ('Exinst.P4' f g)@ +{-# INLINABLE same4 #-} +same4 + :: (SDecide k4, SDecide k3, SDecide k2, SDecide k1) + => (forall a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1) + => f a4 a3 a2 a1 -> g a4 a3 a2 a1 -> x) + -> Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type) + -> Some4 (g :: k4 -> k3 -> k2 -> k1 -> Type) + -> Maybe x -- ^ +same4 z = \s4l s4g -> + withSome4Sing s4l $ \sa4 sa3 sa2 sa1 f -> + withSome4Sing s4g $ \sa4' sa3' sa2' sa1' g -> do + Refl <- testEquality sa4 sa4' + Refl <- testEquality sa3 sa3' + Refl <- testEquality sa2 sa2' + Refl <- testEquality sa1 sa1' + pure (z f g) + +-------------------------------------------------------------------------------- + +-- | 'Dict0' is a bit different from 'Dict1', 'Dict2', etc. in that it looks up +-- an instance for the singleton type itself, and not for some other type +-- indexed by said singleton type. +class Dict0 (c :: k0 -> Constraint) where + -- | Runtime lookup of the @c a0@ instance. + dict0 :: Sing a0 -> Dict (c a0) + +class Dict1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) where + -- | Runtime lookup of the @c (f1 a1)@ instance. + dict1 :: Sing a1 -> Dict (c (f1 a1)) + +class Dict2 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0) where + -- Runtime lookup of the @c (f2 a2 a1)@ instance. + dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1)) + +class Dict3 (c :: k0 -> Constraint) (f3 :: k3 -> k2 -> k1 -> k0) where + -- Runtime lookup of the @c (f3 a3 a2 a1)@ instance. + dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1)) + +class Dict4 (c :: k0 -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> k0) where + -- Runtime lookup of the @c (f4 a4 a3 a2 a1)@ instance. + dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1)) + +-------------------------------------------------------------------------------- +-- Miscelaneous @lens@-compatible stuff. + +type Prism s t a b + = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t) + +type Prism' s a = Prism s s a a + +prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b +prism bt seta = dimap seta (either pure (fmap bt)) . right' +{-# INLINE prism #-} + +prism' :: (b -> s) -> (s -> Maybe a) -> Prism s s a b +prism' bs sma = prism bs (\s -> maybe (Left s) Right (sma s)) +{-# INLINE prism' #-} + diff --git a/lib/Exinst/Internal/Product.hs b/lib/Exinst/Internal/Product.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Internal/Product.hs @@ -0,0 +1,151 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE PolyKinds #-} + +module Exinst.Internal.Product + ( P1(P1) + , P2(P2) + , P3(P3) + , P4(P4) + ) where + +import GHC.Generics (Generic) + +#ifdef HAS_aeson +import Data.Aeson (FromJSON, ToJSON) +#endif + +#ifdef HAS_binary +import qualified Data.Binary as Bin +#endif + +#ifdef HAS_bytes +import qualified Data.Bytes.Serial as By +#endif + +#ifdef HAS_cereal +import qualified Data.Serialize as Cer +#endif + +#ifdef HAS_deepseq +import Control.DeepSeq (NFData) +#endif + +#ifdef HAS_hashable +import Data.Hashable (Hashable) +#endif + +#ifdef HAS_quickcheck +import qualified Test.QuickCheck as QC +#endif + +#ifdef HAS_serialise +import qualified Codec.Serialise as Cborg +#endif + +-------------------------------------------------------------------------------- +-- Products + +-- | Like 'Data.Functor.Product.Product' from "Data.Functor.Product", but +-- only intended to be used with kinds other than 'Type'. +-- +-- This type is particularly useful when used in combination with 'Exinst.Some1' +-- as @'Exinst.Some1' ('P1' l r)@, so as to ensure that @l@ and @r@ are indexed +-- by the same type. Moreover, 'P1' already supports many common instances from +-- @base@, @hashable@, @deepseq@, @aeson@, @bytes@, @cereal@, @binary@, and +-- @quickcheck@ out of the box, so you can benefit from them as well. +data P1 l r (a1 :: k1) + = P1 (l a1) (r a1) + deriving (Eq, Show, Read, Ord, Generic) + +-- | Like 'P1', but for @l@ and @r@ taking two type indexes. +data P2 l r (a2 :: k2) (a1 :: k1) + = P2 (l a2 a1) (r a2 a1) + deriving (Eq, Show, Read, Ord, Generic) + +-- | Like 'P1', but for @l@ and @r@ taking three type indexes. +data P3 l r (a3 :: k3) (a2 :: k2) (a1 :: k1) + = P3 (l a3 a2 a1) (r a3 a2 a1) + deriving (Eq, Show, Read, Ord, Generic) + +-- | Like 'P1', but for @l@ and @r@ taking four type indexes. +data P4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1) + = P4 (l a4 a3 a2 a1) (r a4 a3 a2 a1) + deriving (Eq, Show, Read, Ord, Generic) + +-------------------------------------------------------------------------------- +#ifdef HAS_hashable +instance (Hashable (l a1), Hashable (r a1)) => Hashable (P1 l r a1) +instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (P2 l r a2 a1) +instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (P3 l r a3 a2 a1) +instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (P4 l r a4 a3 a2 a1) +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_deepseq +instance (NFData (l a1), NFData (r a1)) => NFData (P1 l r a1) +instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (P2 l r a2 a1) +instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (P3 l r a3 a2 a1) +instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (P4 l r a4 a3 a2 a1) +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_aeson +instance (FromJSON (l a1), FromJSON (r a1)) => FromJSON (P1 l r a1) +instance (FromJSON (l a2 a1), FromJSON (r a2 a1)) => FromJSON (P2 l r a2 a1) +instance (FromJSON (l a3 a2 a1), FromJSON (r a3 a2 a1)) => FromJSON (P3 l r a3 a2 a1) +instance (FromJSON (l a4 a3 a2 a1), FromJSON (r a4 a3 a2 a1)) => FromJSON (P4 l r a4 a3 a2 a1) + +instance (ToJSON (l a1), ToJSON (r a1)) => ToJSON (P1 l r a1) +instance (ToJSON (l a2 a1), ToJSON (r a2 a1)) => ToJSON (P2 l r a2 a1) +instance (ToJSON (l a3 a2 a1), ToJSON (r a3 a2 a1)) => ToJSON (P3 l r a3 a2 a1) +instance (ToJSON (l a4 a3 a2 a1), ToJSON (r a4 a3 a2 a1)) => ToJSON (P4 l r a4 a3 a2 a1) +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_bytes +instance (By.Serial (l a1), By.Serial (r a1)) => By.Serial (P1 l r a1) +instance (By.Serial (l a2 a1), By.Serial (r a2 a1)) => By.Serial (P2 l r a2 a1) +instance (By.Serial (l a3 a2 a1), By.Serial (r a3 a2 a1)) => By.Serial (P3 l r a3 a2 a1) +instance (By.Serial (l a4 a3 a2 a1), By.Serial (r a4 a3 a2 a1)) => By.Serial (P4 l r a4 a3 a2 a1) +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_cereal +instance (Cer.Serialize (l a1), Cer.Serialize (r a1)) => Cer.Serialize (P1 l r a1) +instance (Cer.Serialize (l a2 a1), Cer.Serialize (r a2 a1)) => Cer.Serialize (P2 l r a2 a1) +instance (Cer.Serialize (l a3 a2 a1), Cer.Serialize (r a3 a2 a1)) => Cer.Serialize (P3 l r a3 a2 a1) +instance (Cer.Serialize (l a4 a3 a2 a1), Cer.Serialize (r a4 a3 a2 a1)) => Cer.Serialize (P4 l r a4 a3 a2 a1) +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_binary +instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (P1 l r a1) +instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (P2 l r a2 a1) +instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (P3 l r a3 a2 a1) +instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (P4 l r a4 a3 a2 a1) +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_quickcheck +instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (P1 l r a1) where + arbitrary = P1 <$> QC.arbitrary <*> QC.arbitrary + shrink (P1 x y) = P1 <$> QC.shrink x <*> QC.shrink y +instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (P2 l r a2 a1) where + arbitrary = P2 <$> QC.arbitrary <*> QC.arbitrary + shrink (P2 x y) = P2 <$> QC.shrink x <*> QC.shrink y +instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (P3 l r a3 a2 a1) where + arbitrary = P3 <$> QC.arbitrary <*> QC.arbitrary + shrink (P3 x y) = P3 <$> QC.shrink x <*> QC.shrink y +instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (P4 l r a4 a3 a2 a1) where + arbitrary = P4 <$> QC.arbitrary <*> QC.arbitrary + shrink (P4 x y) = P4 <$> QC.shrink x <*> QC.shrink y +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_serialise +instance (Cborg.Serialise (l a1), Cborg.Serialise (r a1)) => Cborg.Serialise (P1 l r a1) +instance (Cborg.Serialise (l a2 a1), Cborg.Serialise (r a2 a1)) => Cborg.Serialise (P2 l r a2 a1) +instance (Cborg.Serialise (l a3 a2 a1), Cborg.Serialise (r a3 a2 a1)) => Cborg.Serialise (P3 l r a3 a2 a1) +instance (Cborg.Serialise (l a4 a3 a2 a1), Cborg.Serialise (r a4 a3 a2 a1)) => Cborg.Serialise (P4 l r a4 a3 a2 a1) +#endif diff --git a/lib/Exinst/Internal/Sum.hs b/lib/Exinst/Internal/Sum.hs new file mode 100644 --- /dev/null +++ b/lib/Exinst/Internal/Sum.hs @@ -0,0 +1,155 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE PolyKinds #-} + +module Exinst.Internal.Sum + ( S1(S1L,S1R) + , S2(S2L,S2R) + , S3(S3L,S3R) + , S4(S4L,S4R) + ) where + +import GHC.Generics (Generic) + +#ifdef HAS_aeson +import Data.Aeson (FromJSON, ToJSON) +#endif + +#ifdef HAS_binary +import qualified Data.Binary as Bin +#endif + +#ifdef HAS_bytes +import qualified Data.Bytes.Serial as By +#endif + +#ifdef HAS_cereal +import qualified Data.Serialize as Cer +#endif + +#ifdef HAS_deepseq +import Control.DeepSeq (NFData) +#endif + +#ifdef HAS_hashable +import Data.Hashable (Hashable) +#endif + +#ifdef HAS_quickcheck +import qualified Test.QuickCheck as QC +#endif + +#ifdef HAS_serialise +import qualified Codec.Serialise as Cborg +#endif + +-------------------------------------------------------------------------------- +-- Sums + +-- | Like 'Data.Functor.Sum.Sum' from "Data.Functor.Sum", but +-- only intended to be used with kinds other than 'Type'. +-- +-- This type is particularly useful when used in combination with 'Exinst.Some1' +-- as @'Exinst.Some1' ('S1' l r)@, so as to ensure that @l@ and @r@ are indexed +-- by the same type. Moreover, 'S1' already supports many common instances from +-- @base@, @hashable@, @deepseq@, @aeson@, @bytes@, @cereal@, @binary@, and +-- @quickcheck@ out of the box, so you can benefit from them as well. +data S1 l r (a1 :: k1) + = S1L (l a1) | S1R (r a1) + deriving (Eq, Show, Read, Ord, Generic) + +-- | Like 'S1', but for @l@ and @r@ taking two type indexes. +data S2 l r (a2 :: k2) (a1 :: k1) + = S2L (l a2 a1) | S2R (r a2 a1) + deriving (Eq, Show, Read, Ord, Generic) + +-- | Like 'S1', but for @l@ and @r@ taking three type indexes. +data S3 l r (a3 :: k3) (a2 :: k2) (a1 :: k1) + = S3L (l a3 a2 a1) | S3R (r a3 a2 a1) + deriving (Eq, Show, Read, Ord, Generic) + +-- | Like 'S1', but for @l@ and @r@ taking four type indexes. +data S4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1) + = S4L (l a4 a3 a2 a1) | S4R (r a4 a3 a2 a1) + deriving (Eq, Show, Read, Ord, Generic) + +-------------------------------------------------------------------------------- +#ifdef HAS_hashable +instance (Hashable (l a1), Hashable (r a1)) => Hashable (S1 l r a1) +instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (S2 l r a2 a1) +instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (S3 l r a3 a2 a1) +instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (S4 l r a4 a3 a2 a1) +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_deepseq +instance (NFData (l a1), NFData (r a1)) => NFData (S1 l r a1) +instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (S2 l r a2 a1) +instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (S3 l r a3 a2 a1) +instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (S4 l r a4 a3 a2 a1) +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_aeson +instance (FromJSON (l a1), FromJSON (r a1)) => FromJSON (S1 l r a1) +instance (FromJSON (l a2 a1), FromJSON (r a2 a1)) => FromJSON (S2 l r a2 a1) +instance (FromJSON (l a3 a2 a1), FromJSON (r a3 a2 a1)) => FromJSON (S3 l r a3 a2 a1) +instance (FromJSON (l a4 a3 a2 a1), FromJSON (r a4 a3 a2 a1)) => FromJSON (S4 l r a4 a3 a2 a1) + +instance (ToJSON (l a1), ToJSON (r a1)) => ToJSON (S1 l r a1) +instance (ToJSON (l a2 a1), ToJSON (r a2 a1)) => ToJSON (S2 l r a2 a1) +instance (ToJSON (l a3 a2 a1), ToJSON (r a3 a2 a1)) => ToJSON (S3 l r a3 a2 a1) +instance (ToJSON (l a4 a3 a2 a1), ToJSON (r a4 a3 a2 a1)) => ToJSON (S4 l r a4 a3 a2 a1) +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_bytes +instance (By.Serial (l a1), By.Serial (r a1)) => By.Serial (S1 l r a1) +instance (By.Serial (l a2 a1), By.Serial (r a2 a1)) => By.Serial (S2 l r a2 a1) +instance (By.Serial (l a3 a2 a1), By.Serial (r a3 a2 a1)) => By.Serial (S3 l r a3 a2 a1) +instance (By.Serial (l a4 a3 a2 a1), By.Serial (r a4 a3 a2 a1)) => By.Serial (S4 l r a4 a3 a2 a1) +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_cereal +instance (Cer.Serialize (l a1), Cer.Serialize (r a1)) => Cer.Serialize (S1 l r a1) +instance (Cer.Serialize (l a2 a1), Cer.Serialize (r a2 a1)) => Cer.Serialize (S2 l r a2 a1) +instance (Cer.Serialize (l a3 a2 a1), Cer.Serialize (r a3 a2 a1)) => Cer.Serialize (S3 l r a3 a2 a1) +instance (Cer.Serialize (l a4 a3 a2 a1), Cer.Serialize (r a4 a3 a2 a1)) => Cer.Serialize (S4 l r a4 a3 a2 a1) +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_binary +instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (S1 l r a1) +instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (S2 l r a2 a1) +instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (S3 l r a3 a2 a1) +instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (S4 l r a4 a3 a2 a1) +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_quickcheck +instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (S1 l r a1) where + arbitrary = QC.oneof [ fmap S1L QC.arbitrary, fmap S1R QC.arbitrary ] + shrink (S1L l) = S1L <$> QC.shrink l + shrink (S1R r) = S1R <$> QC.shrink r +instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (S2 l r a2 a1) where + arbitrary = QC.oneof [ fmap S2L QC.arbitrary, fmap S2R QC.arbitrary ] + shrink (S2L l) = S2L <$> QC.shrink l + shrink (S2R r) = S2R <$> QC.shrink r +instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (S3 l r a3 a2 a1) where + arbitrary = QC.oneof [ fmap S3L QC.arbitrary, fmap S3R QC.arbitrary ] + shrink (S3L l) = S3L <$> QC.shrink l + shrink (S3R r) = S3R <$> QC.shrink r +instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (S4 l r a4 a3 a2 a1) where + arbitrary = QC.oneof [ fmap S4L QC.arbitrary, fmap S4R QC.arbitrary ] + shrink (S4L l) = S4L <$> QC.shrink l + shrink (S4R r) = S4R <$> QC.shrink r +#endif + +-------------------------------------------------------------------------------- +#ifdef HAS_serialise +instance (Cborg.Serialise (l a1), Cborg.Serialise (r a1)) => Cborg.Serialise (S1 l r a1) +instance (Cborg.Serialise (l a2 a1), Cborg.Serialise (r a2 a1)) => Cborg.Serialise (S2 l r a2 a1) +instance (Cborg.Serialise (l a3 a2 a1), Cborg.Serialise (r a3 a2 a1)) => Cborg.Serialise (S3 l r a3 a2 a1) +instance (Cborg.Serialise (l a4 a3 a2 a1), Cborg.Serialise (r a4 a3 a2 a1)) => Cborg.Serialise (S4 l r a4 a3 a2 a1) +#endif diff --git a/src/lib/Exinst.hs b/src/lib/Exinst.hs deleted file mode 100644 --- a/src/lib/Exinst.hs +++ /dev/null @@ -1,677 +0,0 @@ -{-# LANGUAGE CPP #-} - -{- | - -Exinst is a library providing you with tools to recover type-indexed types whose -type-indexes have been existentialized, as well as automatically deriving -instances for them, as long as said type indexes are singleton types -(see [singleton](https://hackage.haskell.org/package/singletons)). - -In short, what @exinst@ currently gives you is: For any type @t :: k -> *@, if -@k@ is a singleton type and @c (t a) :: 'Constraint'@ is satisfied, then you can -existentialize away the @a@ parameter with @'Some1' t@, recover it later, and -have @c ('Some1' t)@ automatically satisfied. Currently, up to 4 type indexes -can be existentialized using 'Some1', 'Some2', 'Some3' and 'Some4' respectively. - -NOTE: This tutorial asumes some familiarity with singleton types as implemented -by the [singleton](https://hackage.haskell.org/package/singletons) library. -A singleton type is, in very rough terms, a type inhabited by a single term, -which allows one to go from its term-level representation to its type-level -representation and back without much trouble. A bit like the term @()@, which -is of type @()@. Whenever you have the type @()@ you know what that its -term-level representation must be @()@, and whenever you have the term @()@ -you know that its type must be @()@. - --} - -module Exinst - ( -- * Tutorial - -- $motivation - - -- *** Usage - -- $usage - - -- *** Recovering - -- $recovering - - -- *** Many indexes - -- $manyIndexes - - -- *** Writing instances - -- $writingInstances - - -- *** Products and sums - -- $prodsums - - -- * 1 type index - Some1(Some1) - , some1 - , fromSome1 - , _Some1 - , withSome1 - , withSome1Sing - , some1SingRep - , Dict1(dict1) - - -- * 2 type indexes - , Some2(Some2) - , some2 - , fromSome2 - , _Some2 - , withSome2 - , withSome2Sing - , some2SingRep - , Dict2(dict2) - - -- * 3 type indexes - , Some3(Some3) - , some3 - , fromSome3 - , _Some3 - , withSome3 - , withSome3Sing - , some3SingRep - , Dict3(dict3) - - -- * 4 type indexes - , Some4(Some4) - , some4 - , fromSome4 - , _Some4 - , withSome4 - , withSome4Sing - , some4SingRep - , Dict4(dict4) - - -- * Miscellaneous - , Dict0(dict0) - - -- * Products - , P1(P1) - , P2(P2) - , P3(P3) - , P4(P4) - - -- * Sums - , S1(S1L,S1R) - , S2(S2L,S2R) - , S3(S3L,S3R) - , S4(S4L,S4R) - - -- * Re-exports - , Constraint - , Dict(Dict) - , Sing - , SingI - ) where - -import Data.Constraint (Constraint, Dict(Dict)) - -import Data.Singletons (Sing, SingI) - -import Exinst.Internal -import Exinst.Internal.Product -import Exinst.Internal.Sum - -import Exinst.Instances.Base () - -#ifdef VERSION_aeson -import Exinst.Instances.Aeson () -#endif - -#ifdef VERSION_binary -import Exinst.Instances.Binary () -#endif - -#ifdef VERSION_bytes -import Exinst.Instances.Bytes () -#endif - -#ifdef VERSION_cereal -import Exinst.Instances.Cereal () -#endif - -#ifdef VERSION_deepseq -import Exinst.Instances.DeepSeq () -#endif - -#ifdef VERSION_hashable -import Exinst.Instances.Hashable () -#endif - -#ifdef VERSION_QuickCheck -import Exinst.Instances.QuickCheck () -#endif - - -{- $motivation - -As a motivation, let's consider the following example: - -@ -\{\-\# LANGUAGE GADTs \#\-\} -\{\-\# LANGUAGE DataKinds \#\-\} -\{\-\# LANGUAGE KindSignatures \#\-\} -\{\-\# LANGUAGE FlexibleInstances \#\-\} -\{\-\# LANGUAGE StandaloneDeriving \#\-\} - -data Size = Big | Small - -data Receptacle (a :: Size) :: * where - Vase :: Receptacle 'Small - Glass :: Receptacle 'Small - Barrel :: Receptacle 'Big - -deriving instance 'Show' (Receptacle a) -@ - -@Receptacle@ can describe three types of receptacles (@Vase@, @Glass@ and -@Barrel@), while at the same time being able to indicate, at the type level, -whether the size of the receptacle is @Big@ or @Small@. Additionally, we've -provided 'Show' instances for @Receptacle@. - -Now, if we want to put @Receptacle@s in a container, for example in @[]@, we can -do so only as long as the @Receptacle@ type is fully applied and monomorphic. -That is, we can have @[Receptacle 'Small]@ and @[Receptacle 'Big]@, but we -can't have @[Receptacle]@ nor @[forall a. Receptacle a]@. So, if we want to -have @Receptacle@s of different sizes in a container like @[]@, we need a -different solution. - -At this point we need to ask ourselves why we need to put @Receptacle@s of -different sizes in a same container. If the answer is something like “because we -want to show all of them, no matter what size they are”, then we should realize -that what we are actually asking for is that no matter what @Size@ our -@Receptable@ has, we need to be able to find a 'Show' instance for that -@Receptacle@. In Haskell, we can express just that using existential types -and constraints hidden behind a data constructor. - -@ --- We need to add these language extensions to the ones in the previous example -\{\-\# LANGUAGE ExistentialQuantification \#\-\} -\{\-\# LANGUAGE FlexibleContexts \#\-\} - -data ReceptacleOfAnySizeThatCanBeShown - = forall a. ('Show' (Receptacle a)) - => MkReceptacleOfAnySizeThatCanBeShown (Receptacle a) -@ - -We can construct values of type @ReceptacleOfAnySizeThatCanBeShown@ only as long -as there exist a 'Show' instance for the @Receptacle a@ we give to the -@MkReceptacleOfAnySizeThatCanBeShown@ constructor. In our case, both @Receptacle -'Small@ and @Receptacle 'Big@ have 'Show' instances, so all of @Vase@, @Glass@ and -@Barrel@ can be used successfully with @MkReceptacleOfAnySizeThatCanBeShown@. - -Now, @ReceptacleOfAnySizeThatCanBeShown@ on itself doesn't yet have a 'Show' -instance, and we can't derive one automatically using the @deriving@ mechanism, -but we can give an explicit 'Show' instance that just forwards the work to the -'Show' instance of the underlying @Receptacle a@. - -@ -instance 'Show' ReceptacleOfAnySizeThatCanBeShown where - 'show' (MkReceptacleOfAnySizeThatCanBeShown a) = 'show' a -@ - -That works as intended: - -@ -> 'show' (MkReceptacleOfAnySizeThatCanBeShown Vase) -"Vase" -> 'show' (MkReceptacleOfAnySizeThatCanBeShown Barrel) -"Barrel" -@ - -And now, as we wanted, we can put @Receptacle@s of different sizes in a @[]@ and -show them (as long as we wrap each of them as -@ReceptacleOfAnySizeThatCanBeShown@, that is). - -@ -> 'map' 'show' [MkReceptacleOfAnySizeThatCanBeShown Vase, MkReceptacleOfAnySizeThatCanBeShown Barrel] -["Vase", "Barrel"] -@ - -However, the above solution is unsatisfying for various reasons: For one, the -'Show' instance for @ReceptacleOfAnySizeThatCanBeShown@ works only as long as -the @ReceptacleOfAnySizeThatCanBeShown@ itself carries a witness that the 'Show' -constraint for @Receptacle a@ is satisfied, which means that if we want to write -yet another instance for @ReceptacleOfAnySizeThatCanBeShown@ that simply forwards -its implementation to the underlying @Receptacle a@, say 'Eq', then the -@MkReceptacleOfAnySizeThatCanBeShown@ constructor would need to be modified to witness -the @Eq (Receptacle a)@ instance too: - -@ -data ReceptacleOfAnySizeThatCanBeShown - = forall a. ('Show' (Receptacle a), 'Eq' (Receptacle a)) - => MkReceptacleOfAnySizeThatCanBeShown (Receptacle a) -@ - -With that in place we can provide an 'Eq' instance for -@ReceptacleOfAnySizeThatCanBeShown@ as we did for 'Show' before, but if we pay -close attention, we can see how the implementation of -@ReceptacleOfAnySizeThatCanBeShown@ starts to become a bottleneck: Every -instance we want to provide for @ReceptacleOfAnySizeThatCanBeShown@ that simply -forwards its work to the underlying @Receptacle a@ needs to be witnessed by -@MkReceptacleOfAnySizeThatCanBeShown@ itself, it is not enough that there exists -an instance for @Receptacle a@. Moreover, even the name -@ReceptacleOfAnySizeThatCanBeShown@ that we chose before isn't completely -accurate anymore, and will become less and less accurate as we continue adding -constraints to @MkReceptacleOfAnySizeThatCanBeShown@. - -Additionally, everywhere we use the @MkReceptacleOfAnySizeThatCanBeShown@ -constructor we need to witness that the existentialized @Receptacle a@ satisfies -all the required constraints, which means that, if the @Receptacle a@ we pass to -@MkReceptacleOfAnySizeThatCanBeShown@ is being received, say, as a parameter to -a function, then the type of that function will also require that its caller -satisfies all of the same constraints, even though it is obvious to us, -statically, that the instances exist. We can now see how all of this becomes -unmanegeable, or at least very *boilerplatey*, as those constraints start to -propagate through our code base. - -What we need is a way for instances such as the 'Show' instance for -@ReceptacleOfAnySizeThatCanBeShown@ to find the 'Show' instance for @Receptacle -a@ without it being explicitely witnessed by the -@MkReceptacleOfAnySizeThatCanBeShown@ constructor. That is exactly the problem -that @exinst@ solves: allowing /exi/stentials to find their /inst/ances. Thus, -the name of this library. - --} - -{- $usage - -Given the code for @Size@, @Receptacle@ and its 'Show' instances above, we can -achieve the same functionality as our initial @ReceptacleOfAnySizeThatCanBeShown@ by -existentializing the type indexes of @Receptacle 'Small@ and @Receptacle 'Big@ -as @'Some1' Receptacle@. In order to do that, we must first ensure that @Size@ and its -constructors can be used as singleton types (as supported by the @singletons@ library), -for which we can use some @TemplateHaskell@ provided by @Data.Singletons.TH@: - -@ -import qualified "Data.Singletons.TH" - -Data.Singletons.TH.genSingletons [''Size] -@ - -And we'll also need a 'Show' instance for @Size@ for reasons that will become -apparent later: - -@ -deriving instance 'Show' Size -@ - -Now we can construct a @Show1 Size@ and 'show' achieving the same results as we -did with @ReceptacleOfAnySizeThatCanBeShown@ before. - -Note: this code won't work yet. Keep reading. - -@ -> import "Exinst" ('Some1', 'some1') -> :t 'some1' Glass -:t 'some1' Glass :: 'Some1' Receptacle -> 'show' ('some1' Glass) -"Some1 Small Glass" -@ - -Well, actually, the default 'Show' instance for 'Some1' shows a bit more of -information, as it permits this string to be 'Read' back into a @'Some1' -Receptacle@ if needed, but displaying just @"Glass"@ would be possible too, if -desired. - -The important thing to notice in the example above is that @some1@ does not -require us to satisfy a @'Show' (Receptacle 'Small)@ constraint, it just requires -that the type index for the type-indexed type we give it as argument is a -singleton type: - -@ -'some1' :: forall (f1 :: k1 -> *) (a1 :: k1). 'SingI' a1 => f1 a1 -> 'Some1' f1 -@ - -It is the application of 'show' to @'some1' Glass@ which will fail to compile if -there isn't a 'Show' instance for @Receptacle 'Small@, complaining that a 'Show' -instance for @'Some1' Receptable@ can't be found. The reason for this is that even -if 'Show' instances for 'Some1' are derived for free, they are only derived for -@'Some1' (t :: k1 -> *)@ where a @'Show' (t a)@ for a specific but statically -unknown @a@ can be found at runtime (mostly, there are other minor requirements too). -The mechanism through which instances are found at runtime relies on 'Dict' from -the [constraints](https://hackage.haskell.org/package/constraints) library, which -@exinst@ wraps in a 'Dict1' typeclass to be instantiated once per singleton -type. - -@ --- The "Exinst.Dict1" class -class 'Dict1' (c :: k0 -> 'Constraint') (f1 :: k1 -> k0) where - 'dict1' :: 'Sing' (a1 :: k1) -> 'Dict' (c (f1 a1)) -@ - -What 'Dict1' says is that: for a type-indexed type @f1@, given a term-level -representation of the singleton type that indexes said @f1@, we can obtain a -witness that the constraint @c@ is satisfied by @f1@ applied to the singleton -type. - -That class seems to be a bit too abstract, but the instances we as users need to -write for it are quite silly and straightforward. - -Here's an example of how to provide 'Show' support for @'Some1' Receptacle@ via -'Dict1': - -@ -instance ('Show' (Receptacle 'Small), 'Show' (Receptacle 'Big)) => 'Dict1' 'Show' Receptacle where - 'dict1' = \x -> case x of - SSmall -> 'Dict' - SBig -> 'Dict' -@ - -The implementation of @dict1@ looks quite silly, but it has to look like that as -it is only by pattern-matching on each of the @'Sing' Size@ constructors that we -learn about the type level representation of a singleton type, which we then use -to select the proper 'Show' instance among all of those listed in the instance head. - -Given this 'Dict1' instance, we can proceed to excecute the REPL example mentioned before -and it will work just fine. - -However, that 'Dict1' instance is still a bit insatisfactory: If we wanted, -again, to provide 'Eq' support for our @'Some1' Receptacle@ type, we would need to -write yet another 'Dict1' instance like the one above, but mentioning 'Eq' -instead of 'Show'. We can do better. - -The trick, when writing 'Dict1' instances such as the one above, is to leave @c@ -and @f1 :: k1 -> k0@ completely polymorphic, and instead only talk concretely -about the singleton type with kind @k1@. This might sound strange at first, as -@c@ and @f1@ are the only two type parameters to 'Dict1'. But as it often happens -when working with singleton types, we are not particularly interested in the -types involved, but in their kinds instead. So, this is the 'Dict1' instance -you often want to write: - -@ -instance (c (f1 'Small), c (f1 'Big)) => 'Dict1' c (f1 :: Size -> k0) where - 'dict1' = \x -> case x of - SSmall -> 'Dict' - SBig -> 'Dict' -@ - -That instance says that for any choice of @c@ and @f1 :: Size -> k0@, if an -instance for @c (f1 a)@ exists for a specific choice of @a@, then, given a term -level representation for that @a@ and the aid of @dict1@, said instance can be -looked up at runtime. - -Notice that 'Some1' itself doesn't have any requirements about 'Dict1', it's the -various instances for 'Some1' who rely on 'Dict1'. 'Dict1' has nothing to do -with 'Some1', nor with the choice of @f@ nor with the choice of @c@; it is only -related to the singleton type used as a type-index for @f@. - -The @Exinst@ module exports ready-made instances for 'Some1', 'Some2', 'Some3' -and 'Some4' (they can be enabled or disabled with some cabal flags). - -* 'Eq', 'Ord', 'Show' from the @base@ package. - -* 'Data.Aeson.FromJSON' and 'Data.Aeson.ToJSON' from the @aeson@ package. - -* 'Data.Bytes.Serial' from the @bytes@ package. - -* 'Cereal.Serialize.Serialize' from the @cereal@ package. - -* 'Data.Binary.Binary' from the @binary@ package. - -* 'Data.Hashable.Hashable' from the @hashable@ package. - -* 'Control.DeepSeq.NFData' from the @deepseq@ package. - -* 'Test.QuickCheck.Arbitrary' from the @QuickCheck@ package. - -You are invited to read the instance heads for said instances so as to understand -what you need to provide in order to get those instances “for free”. As a rule of -thumb, most instances will require this: If you expect to have an instance for -@class Y => Z a@ satisfied for @'Some1' (f :: k1 -> *)@, then make sure an instance -for @Z@ is available for the @DemoteRep k1@, that a @'Dict1' Z (f :: k1 -> k0)@ or -more general instance exists, and that the @Y@ instance for @'Some1' (f :: k1 -> -*)@ exists too. - -Here is the full code needed to have, say, the 'Eq' and 'Show' instances -available for @'Some1' Receptacle@: - -@ -\{\-\# LANGUAGE ConstraintKinds \#\-\} -\{\-\# LANGUAGE DataKinds \#\-\} -\{\-\# LANGUAGE FlexibleInstances \#\-\} -\{\-\# LANGUAGE GADTs \#\-\} -\{\-\# LANGUAGE KindSignatures \#\-\} -\{\-\# LANGUAGE MultiParamTypeClasses \#\-\} -\{\-\# LANGUAGE OverloadedStrings \#\-\} -\{\-\# LANGUAGE StandaloneDeriving \#\-\} -\{\-\# LANGUAGE TemplateHaskell \#\-\} -\{\-\# LANGUAGE TypeFamilies \#\-\} -\{\-\# LANGUAGE UndecidableInstances \#\-\} - -import qualified "Data.Singletons.TH" -import "Exinst" ('Dict'('Dict'), 'Dict1'('dict1')) - -data Size = Big | Small - deriving ('Eq', 'Show') - -Data.Singletons.TH.genSingletons [''Size] -Data.Singletons.TH.singDecideInstances [''Size] - -instance (c (f 'Big), c (f 'Small)) => 'Dict1' c f where - 'dict1' = \x -> case x of - SBig -> 'Dict' - SSmall -> 'Dict' - - -data Receptacle (a :: Size) :: * where - Vase :: Receptacle 'Small - Glass :: Receptacle 'Small - Barrel :: Receptacle 'Big - -deriving instance 'Eq' (Receptacle a) -deriving instance 'Show' (Receptacle a) -@ - -Now, @'Some1' Receptacle@ will have 'Eq' and 'Show' instances: - -@ -> -- Trying 'fromSome1'. -> 'fromSome1' ('some1' Vase) == 'Just' Vase -'True' -> 'fromSome1' ('some1' Vase) == 'Just' Glass -'False' -> 'fromSome1' ('some1' Vase) == 'Just' Barrel -'False' - -> -- Trying 'withSome1' -> 'withSome1' ('some1' Vase) 'show' -"Vase" -> 'withSome1' ('some1' Vase) (== Vase) -- This will fail, use 'fromSome1' - -- if you know you are expecting - -- a @Receptacle 'Small@ - -> -- Trying the 'Eq' instance. -> 'some1' Vase == 'some1' Vase -'True' -> 'some1' Vase == 'some1' Glass -'False' -> 'some1' Vase == 'some1' Barrel -'False' - -> -- Trying the 'Show' instance. -> 'show' ('some1' Vase) -"Some1 Small Vase" -> 'map' 'show' ['some1' Vase, 'some1' Glass, 'some1' Barrel] -["Some1 Small Vase","Some1 Small Glass","Some1 Big Barrel"] -@ - --} - -{- $manyIndexes - -Just like 'Some1' hides the last singleton type index from fully applied -type-indexed type, 'Some2' hides the last two type indexes, 'Some3' hides the -last three, and 'Some3' hides the last four. They can be used in the same way as -'Some1'. - -Like as most instances for 'Some1' require 'Dict1' instances to be present for -their singleton type-index, most instances for 'Some2', 'Some3' and 'Some4' will -require that 'Dict2', 'Dict3' or 'Dict4' instances exist, respectively. Writing -these instances is very straightforward. Supposing you have a type @X :: T4 -> -T3 -> T2 -> T1 -> *@ and want to existentialize all of the four type indexes yet -be able to continue using all of its instances, we can write something like -this: - -@ -instance (c (f1 'T1a), c (f1 'T1b)) => 'Dict1' c (f1 :: T1 -> k0) where - 'dict1' = \x -> case x of { ST1a -> 'Dict'; ST1b -> 'Dict' } -instance ('Dict1' c (f2 'T2a), 'Dict1' c (f2 'T2b)) => 'Dict2' c (f2 :: T2 -> k1 -> k0) where - 'dict2' = \x -> case x of { ST2a -> 'dict1'; ST2b -> 'dict1' } -instance ('Dict2' c (f3 'T3a), 'Dict2' c (f3 'T3b)) => 'Dict3' c (f3 :: T3 -> k2 -> k1 -> k0) where - 'dict3' = \x -> case x of { ST3a -> 'dict2'; ST3b -> 'dict2' } -instance ('Dict3' c (f4 'T4a), 'Dict3' c (f4 'T4b)) => 'Dict4' c (f4 :: T4 -> k3 -> k2 -> k1 -> k0) where - 'dict4' = \x -> case x of { ST4a -> 'dict3'; ST4b -> 'dict3' } -@ - -That is, assuming the following @T1@, @T2@, @T3@ and @T4@: - -@ -data T4 = T4a | T4b -data T3 = T3a | T3b -data T2 = T2a | T2b -data T1 = T1a | T1b -@ - -Effectively, we wrote just one instance per singleton type per type-index -position, each of them promoting a term-level representation of a singleton -type to its type-level representation and forwarding the rest of the work to -a “smaller” dict. That is, 'dict4' reifies the type of the fourth-to-last -type-index of @X@ and then calls 'dict3' to do the same for the third-to-last -type-index of @X@ and so on. Notice, however, how we didn't need to mention @X@ -in none of the instances above: As we said before, these instances are -intended to work for any choice of @c@, @f4@, @f3@, @f2@ and @f1@. - --} - -{- $recovering - -If you have a @'Some1' (f :: k -> *)@ and you know, statically, that you need an -specific @f (a :: k)@, then you can use 'fromSome1' which will give you an -@f (a :: k)@ only if @a@ was the type that was existentialized by 'Some1'. -Using 'fromSome1' requires that the singleton type-index implements -'Data.Singletons.Decide.SDecide', which can be derived mechanically with -`TemplateHaskell` by means of 'Data.Singletons.TH.singInstance'. - -If you don't know, statically, the type of @f (a :: k)@, then you can use -'withSome1Sing' or 'withSome1' to work with @f (a :: k)@ as long as @a@ never -leaves their scope (don't worry, the compiler will yell at you if you try to do -that). - --} - - -{- $prodsums - -Consider the following types and constructors: - -@ -data X (a :: 'Bool') where - XT :: X ''True' - XF :: X ''False' - -data Y (a :: 'Bool') where - YT :: Y ''True' - YF :: Y ''False' -@ - -You can use '(,)' to create a product for values of this type, and 'Either' to -create a sum. However, see what happens if we try to existentialize the type -index when using that approach: - -@ -> :t ('some1' XT, 'some1' YT) -('some1' XT, 'some1' YT) :: ('Some1' X, 'Some1' Y) -> :t ('some1' XT, 'some1' YF) -('some1' XT, 'some1' YF) :: ('Some1' X, 'Some1' Y) -@ - -It works, but there is no type level guarantee that the type index taken by @X@ -and @Y@ is the same. If you do want to enforce that restriction, then you can -use @P1@ instead: - -@ -> :t 'P1' -'P1' :: l a -> r a -> 'P1' l r (a :: k) -> :t 'P1' XT YT -'P1' XT YT :: 'P1' X Y ''True' -> :t 'P1' XT YT -'P1' XT YT :: 'P1' X Y ''True' -> :t 'some1' ('P1' XT YT) -'some1' ('P1' XT YT) :: 'Some1' ('P1' X Y) -@ - -Trying to mix @XT@ with @YF@ fails, of course, since they have different type -indexes: - -@ -> :t 'P1' XT YF -\:1:7: error: - • Couldn't match type ‘''False'’ with ‘''True'’ - Expected type: Y ''True' - Actual type: Y ''False' - • In the second argument of ‘'P1'’, namely ‘YF’ - In the expression: 'P1' XT YF -@ - -Moreover, 'P1' supports many common instances from @base@, @hashable@, -@deepseq@, @aeson@, @bytes@, @cereal@, @binary@ and @quickcheck@ out of the -box, so you can benefit from them as well. - -There's also 'P2', 'P3' and 'P4' for product types taking a different number of -indexes, and also 'S1', 'S2', 'S3' and 'S4' for sum types: - -@ -> :t 'S1L' -'S1L' :: l a -> 'S1' l r (a :: k) -> :t 'S1R' -'S1R' :: r a -> 'S1' l r (a :: k) -> :t 'S1L' XT -'S1L' XT :: 'S1' X r ''True' -> :t 'S1R' YT -'S1R' YT :: 'S1' l Y ''True' -> :t 'some1' ('S1L' XT) -'some1' ('S1L' XT) :: 'Some1' ('S1' X r) -> :t 'some1' ('S1R' YT) -'some1' ('S1R' YT) :: 'Some1' ('S1' l Y) -@ - --} - - -{- $writingInstances - -Instances for 'Some1' seem to come out of thin air, but the truth is that they -need to be written at least once by library authors so that, provided all its -requirements are satisfied, they are made available. - -For example, when we imported "Exinst" before, we also brought to scope, among -other things, the 'Eq' instance for 'Some1', which is defined as this: - -@ -instance forall (f :: k1 -> *). - ( 'Data.Singletons.Decide.SDecide' k1 - , 'Dict1' 'Eq' f - ) => 'Eq' ('Some1' f) - where - (==) = \\som1x som1y -> - 'withSome1Sing' som1x $ \\sa1x (x :: f a1x) -> - 'withSome1Sing' som1y $ \\sa1y (y :: f a1y) -> - 'maybe' 'False' 'id' $ do - 'Data.Type.Equality.Refl' <- 'Data.Type.Equality.testEquality' sa1x sa1y - case 'dict1' sa1x :: 'Dict' ('Eq' (f a1x)) of - 'Dict' -> 'Just' (x == y) -@ - -This code should be relatively straightforward if you are familiar with uses of -the @singletons@ and @constraints@ libraries. We are simply reifying singleton -types from their term-level representation to their type-level representation, -and afterwards using the 'Dict1' mechanism to lookup the required instances -during runtime. Additionaly, this instance requires that the term level -representation of the singleton type implements 'Show' too, as, like we saw in a -previous example, the type index itself is shown in this 'Show' implementation, -in the hope that it can be later recovered and reified to the type level when -using 'Read'. - --} diff --git a/src/lib/Exinst/Instances/Aeson.hs b/src/lib/Exinst/Instances/Aeson.hs deleted file mode 100644 --- a/src/lib/Exinst/Instances/Aeson.hs +++ /dev/null @@ -1,159 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'Ae.FromJSON' and 'Ae.ToJSON' instances for 'Some1', --- 'Some2', 'Some3' and 'Some4' from "Exinst", provided situable --- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.Aeson () where - -import qualified Data.Aeson as Ae -import Data.Constraint -import Data.Singletons -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - -instance forall (f :: k1 -> *) - . ( SingKind k1 - , Ae.ToJSON (DemoteRep k1) - , Dict1 Ae.ToJSON f - ) => Ae.ToJSON (Some1 f) - where - {-# INLINABLE toJSON #-} - toJSON = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (Ae.ToJSON (f a1)) of - Dict -> Ae.toJSON (fromSing sa1, x) - -instance forall (f :: k2 -> k1 -> *) - . ( SingKind k2 - , SingKind k1 - , Ae.ToJSON (DemoteRep k2) - , Ae.ToJSON (DemoteRep k1) - , Dict2 Ae.ToJSON f - ) => Ae.ToJSON (Some2 f) - where - {-# INLINABLE toJSON #-} - toJSON = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (Ae.ToJSON (f a2 a1)) of - Dict -> Ae.toJSON ((fromSing sa2, fromSing sa1), x) - -instance forall (f :: k3 -> k2 -> k1 -> *) - . ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Ae.ToJSON (DemoteRep k3) - , Ae.ToJSON (DemoteRep k2) - , Ae.ToJSON (DemoteRep k1) - , Dict3 Ae.ToJSON f - ) => Ae.ToJSON (Some3 f) - where - {-# INLINABLE toJSON #-} - toJSON = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f a3 a2 a1)) of - Dict -> Ae.toJSON ((fromSing sa3, fromSing sa2, fromSing sa1), x) - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> *) - . ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Ae.ToJSON (DemoteRep k4) - , Ae.ToJSON (DemoteRep k3) - , Ae.ToJSON (DemoteRep k2) - , Ae.ToJSON (DemoteRep k1) - , Dict4 Ae.ToJSON f - ) => Ae.ToJSON (Some4 f) - where - {-# INLINABLE toJSON #-} - toJSON = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f a4 a3 a2 a1)) of - Dict -> Ae.toJSON ((fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1), x) - --------------------------------------------------------------------------------- - -instance forall (f :: k1 -> *) - . ( SingKind k1 - , Ae.FromJSON (DemoteRep k1) - , Dict1 Ae.FromJSON f - ) => Ae.FromJSON (Some1 f) - where - {-# INLINABLE parseJSON #-} - parseJSON = \v -> do - (rsa1, v') <- Ae.parseJSON v - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (Ae.FromJSON (f a1)) of - Dict -> do - x :: f a1 <- Ae.parseJSON v' - pure (Some1 sa1 x) - -instance forall (f :: k2 -> k1 -> *) - . ( SingKind k2 - , SingKind k1 - , Ae.FromJSON (DemoteRep k2) - , Ae.FromJSON (DemoteRep k1) - , Dict2 Ae.FromJSON f - ) => Ae.FromJSON (Some2 f) - where - {-# INLINABLE parseJSON #-} - parseJSON = \v -> do - ((rsa2, rsa1), v') <- Ae.parseJSON v - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (Ae.FromJSON (f a2 a1)) of - Dict -> do - x :: f a2 a1 <- Ae.parseJSON v' - pure (Some2 sa2 sa1 x) - -instance forall (f :: k3 -> k2 -> k1 -> *) - . ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Ae.FromJSON (DemoteRep k3) - , Ae.FromJSON (DemoteRep k2) - , Ae.FromJSON (DemoteRep k1) - , Dict3 Ae.FromJSON f - ) => Ae.FromJSON (Some3 f) - where - {-# INLINABLE parseJSON #-} - parseJSON = \v -> do - ((rsa3, rsa2, rsa1), v') <- Ae.parseJSON v - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f a3 a2 a1)) of - Dict -> do - x :: f a3 a2 a1 <- Ae.parseJSON v' - pure (Some3 sa3 sa2 sa1 x) - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> *) - . ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Ae.FromJSON (DemoteRep k4) - , Ae.FromJSON (DemoteRep k3) - , Ae.FromJSON (DemoteRep k2) - , Ae.FromJSON (DemoteRep k1) - , Dict4 Ae.FromJSON f - ) => Ae.FromJSON (Some4 f) - where - {-# INLINABLE parseJSON #-} - parseJSON = \v -> do - ((rsa4, rsa3, rsa2, rsa1), v') <- Ae.parseJSON v - withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f a4 a3 a2 a1)) of - Dict -> do - x :: f a4 a3 a2 a1 <- Ae.parseJSON v' - pure (Some4 sa4 sa3 sa2 sa1 x) diff --git a/src/lib/Exinst/Instances/Base.hs b/src/lib/Exinst/Instances/Base.hs deleted file mode 100644 --- a/src/lib/Exinst/Instances/Base.hs +++ /dev/null @@ -1,622 +0,0 @@ -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'Show', 'Eq' and 'Ord' instances for 'Exinst.Some1', --- 'Exinst.Some2', 'Exinst.Some3' and 'Exinst.Some4' from "Exinst", provided situable --- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available. --- --- See the README file for more general documentation: https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.Base () where - -import Data.Constraint -import Data.Kind (Type) -import Data.Singletons -import Data.Singletons.Prelude.Enum (PEnum(EnumFromTo), PBounded(MinBound, MaxBound)) -import Data.Singletons.Prelude.Bool (Sing(STrue,SFalse)) -import qualified Data.Singletons.Prelude.List as List -import Data.Singletons.Prelude.Tuple (Tuple2Sym1) -import Data.Singletons.Decide -import Data.Type.Equality -import qualified GHC.Generics as G -import Prelude -import qualified Text.Read as Read - -import Exinst.Internal - hiding (Some1(..), Some2(..), Some3(..), Some4(..)) -import qualified Exinst.Internal as Exinst - --------------------------------------------------------------------------------- --- Show - --- Internal wrappers used to avoid writing the string manipulation in 'Show'. -data Some1'Show r1 x = Some1 r1 x deriving (Show) -data Some2'Show r2 r1 x = Some2 r2 r1 x deriving (Show) -data Some3'Show r3 r2 r1 x = Some3 r3 r2 r1 x deriving (Show) -data Some4'Show r4 r3 r2 r1 x = Some4 r4 r3 r2 r1 x deriving (Show) - -instance forall (f :: k1 -> Type) - . ( SingKind k1 - , Show (DemoteRep k1) - , Dict1 Show f - ) => Show (Exinst.Some1 f) - where - {-# INLINABLE showsPrec #-} - showsPrec n = \some1x -> withSome1Sing some1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (Show (f a1)) of - Dict -> showsPrec n (Some1 (fromSing sa1) x) - -instance forall (f :: k2 -> k1 -> Type) - . ( SingKind k2 - , SingKind k1 - , Show (DemoteRep k2) - , Show (DemoteRep k1) - , Dict2 Show f - ) => Show (Exinst.Some2 f) - where - {-# INLINABLE showsPrec #-} - showsPrec n = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (Show (f a2 a1)) of - Dict -> showsPrec n (Some2 (fromSing sa2) (fromSing sa1) x) - -instance forall (f :: k3 -> k2 -> k1 -> Type) - . ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Show (DemoteRep k3) - , Show (DemoteRep k2) - , Show (DemoteRep k1) - , Dict3 Show f - ) => Show (Exinst.Some3 f) - where - {-# INLINABLE showsPrec #-} - showsPrec n = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Show (f a3 a2 a1)) of - Dict -> showsPrec n (Some3 (fromSing sa3) (fromSing sa2) (fromSing sa1) x) - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) - . ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Show (DemoteRep k4) - , Show (DemoteRep k3) - , Show (DemoteRep k2) - , Show (DemoteRep k1) - , Dict4 Show f - ) => Show (Exinst.Some4 f) - where - {-# INLINABLE showsPrec #-} - showsPrec n = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Show (f a4 a3 a2 a1)) of - Dict -> showsPrec n (Some4 (fromSing sa4) (fromSing sa3) - (fromSing sa2) (fromSing sa1) x) - --------------------------------------------------------------------------------- --- Read - -instance forall (f :: k1 -> Type) - . ( SingKind k1 - , Read (DemoteRep k1) - , Dict1 Read f - ) => Read (Exinst.Some1 f) - where - {-# INLINABLE readPrec #-} - readPrec = do - Read.Ident "Some1" <- Read.lexP - rsa1 <- Read.readPrec - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (Read (f a1)) of - Dict -> do - x :: f a1 <- Read.readPrec - pure (Exinst.Some1 sa1 x) - -instance forall (f :: k2 -> k1 -> Type) - . ( SingKind k2 - , SingKind k1 - , Read (DemoteRep k2) - , Read (DemoteRep k1) - , Dict2 Read f - ) => Read (Exinst.Some2 f) - where - {-# INLINABLE readPrec #-} - readPrec = do - Read.Ident "Some2" <- Read.lexP - rsa2 <- Read.readPrec - rsa1 <- Read.readPrec - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (Read (f a2 a1)) of - Dict -> do - x :: f a2 a1 <- Read.readPrec - pure (Exinst.Some2 sa2 sa1 x) - -instance forall (f :: k3 -> k2 -> k1 -> Type) - . ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Read (DemoteRep k3) - , Read (DemoteRep k2) - , Read (DemoteRep k1) - , Dict3 Read f - ) => Read (Exinst.Some3 f) - where - {-# INLINABLE readPrec #-} - readPrec = do - Read.Ident "Some3" <- Read.lexP - rsa3 <- Read.readPrec - rsa2 <- Read.readPrec - rsa1 <- Read.readPrec - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (Read (f a3 a2 a1)) of - Dict -> do - x :: f a3 a2 a1 <- Read.readPrec - pure (Exinst.Some3 sa3 sa2 sa1 x) - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) - . ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Read (DemoteRep k4) - , Read (DemoteRep k3) - , Read (DemoteRep k2) - , Read (DemoteRep k1) - , Dict4 Read f - ) => Read (Exinst.Some4 f) - where - {-# INLINABLE readPrec #-} - readPrec = do - Read.Ident "Some4" <- Read.lexP - rsa4 <- Read.readPrec - rsa3 <- Read.readPrec - rsa2 <- Read.readPrec - rsa1 <- Read.readPrec - withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Read (f a4 a3 a2 a1)) of - Dict -> do - x :: f a4 a3 a2 a1 <- Read.readPrec - pure (Exinst.Some4 sa4 sa3 sa2 sa1 x) - --------------------------------------------------------------------------------- --- Eq - -instance forall (f :: k1 -> Type). - ( SDecide k1 - , Dict1 Eq f - ) => Eq (Exinst.Some1 f) - where - {-# INLINABLE (==) #-} - (==) = \som1x som1y -> - withSome1Sing som1x $ \sa1x (x :: f a1x) -> - withSome1Sing som1y $ \sa1y (y :: f a1y) -> - maybe False id $ do - Refl <- testEquality sa1x sa1y - case dict1 sa1x :: Dict (Eq (f a1x)) of - Dict -> Just (x == y) - -instance forall (f :: k2 -> k1 -> Type) - . ( SDecide k2 - , SDecide k1 - , Dict2 Eq f - ) => Eq (Exinst.Some2 f) - where - {-# INLINABLE (==) #-} - (==) = \som2x som2y -> - withSome2Sing som2x $ \sa2x sa1x (x :: f a2x a1x) -> - withSome2Sing som2y $ \sa2y sa1y (y :: f a2y a1y) -> - maybe False id $ do - Refl <- testEquality sa2x sa2y - Refl <- testEquality sa1x sa1y - case dict2 sa2x sa1x :: Dict (Eq (f a2x a1x)) of - Dict -> Just (x == y) - -instance forall (f :: k3 -> k2 -> k1 -> Type) - . ( SDecide k3 - , SDecide k2 - , SDecide k1 - , Dict3 Eq f - ) => Eq (Exinst.Some3 f) - where - {-# INLINABLE (==) #-} - (==) = \som3x som3y -> - withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f a3x a2x a1x) -> - withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f a3y a2y a1y) -> - maybe False id $ do - Refl <- testEquality sa3x sa3y - Refl <- testEquality sa2x sa2y - Refl <- testEquality sa1x sa1y - case dict3 sa3x sa2x sa1x :: Dict (Eq (f a3x a2x a1x)) of - Dict -> Just (x == y) - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) - . ( SDecide k4 - , SDecide k3 - , SDecide k2 - , SDecide k1 - , Dict4 Eq f - ) => Eq (Exinst.Some4 f) - where - {-# INLINABLE (==) #-} - (==) = \som4x som4y -> - withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f a4x a3x a2x a1x) -> - withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f a4y a3y a2y a1y) -> - maybe False id $ do - Refl <- testEquality sa4x sa4y - Refl <- testEquality sa3x sa3y - Refl <- testEquality sa2x sa2y - Refl <- testEquality sa1x sa1y - case dict4 sa4x sa3x sa2x sa1x :: Dict (Eq (f a4x a3x a2x a1x)) of - Dict -> Just (x == y) - --------------------------------------------------------------------------------- --- Ord - -instance forall (f :: k1 -> Type) - . ( SingKind k1 - , SDecide k1 - , Ord (DemoteRep k1) - , Dict1 Ord f - , Eq (Exinst.Some1 f) - ) => Ord (Exinst.Some1 f) - where - {-# INLINABLE compare #-} - compare = \som1x som1y -> - withSome1Sing som1x $ \sa1x (x :: f a1x) -> - withSome1Sing som1y $ \sa1y (y :: f a1y) -> - let termCompare = compare (fromSing sa1x) (fromSing sa1y) - in maybe termCompare id $ do - Refl <- testEquality sa1x sa1y - case dict1 sa1x :: Dict (Ord (f a1x)) of - Dict -> Just (compare x y) - -instance forall (f :: k2 -> k1 -> Type) - . ( SingKind k2 - , SingKind k1 - , SDecide k2 - , SDecide k1 - , Ord (DemoteRep k2) - , Ord (DemoteRep k1) - , Dict2 Ord f - , Eq (Exinst.Some2 f) - ) => Ord (Exinst.Some2 f) - where - {-# INLINABLE compare #-} - compare = \som2x som2y -> - withSome2Sing som2x $ \sa2x sa1x (x :: f a2x a1x) -> - withSome2Sing som2y $ \sa2y sa1y (y :: f a2y a1y) -> - let termCompare = compare (fromSing sa2x, fromSing sa1x) - (fromSing sa2y, fromSing sa1y) - in maybe termCompare id $ do - Refl <- testEquality sa2x sa2y - Refl <- testEquality sa1x sa1y - case dict2 sa2x sa1x :: Dict (Ord (f a2x a1x)) of - Dict -> Just (compare x y) - -instance forall (f :: k3 -> k2 -> k1 -> Type) - . ( SingKind k3 - , SingKind k2 - , SingKind k1 - , SDecide k3 - , SDecide k2 - , SDecide k1 - , Ord (DemoteRep k3) - , Ord (DemoteRep k2) - , Ord (DemoteRep k1) - , Dict3 Ord f - , Eq (Exinst.Some3 f) - ) => Ord (Exinst.Some3 f) - where - {-# INLINABLE compare #-} - compare = \som3x som3y -> - withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f a3x a2x a1x) -> - withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f a3y a2y a1y) -> - let termCompare = compare - (fromSing sa3x, fromSing sa2x, fromSing sa1x) - (fromSing sa3y, fromSing sa2y, fromSing sa1y) - in maybe termCompare id $ do - Refl <- testEquality sa3x sa3y - Refl <- testEquality sa2x sa2y - Refl <- testEquality sa1x sa1y - case dict3 sa3x sa2x sa1x :: Dict (Ord (f a3x a2x a1x)) of - Dict -> Just (compare x y) - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) - . ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , SDecide k4 - , SDecide k3 - , SDecide k2 - , SDecide k1 - , Ord (DemoteRep k4) - , Ord (DemoteRep k3) - , Ord (DemoteRep k2) - , Ord (DemoteRep k1) - , Dict4 Ord f - , Eq (Exinst.Some4 f) - ) => Ord (Exinst.Some4 f) - where - {-# INLINABLE compare #-} - compare = \som4x som4y -> - withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f a4x a3x a2x a1x) -> - withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f a4y a3y a2y a1y) -> - let termCompare = compare - (fromSing sa4x, fromSing sa3x, fromSing sa2x, fromSing sa1x) - (fromSing sa4y, fromSing sa3y, fromSing sa2y, fromSing sa1y) - in maybe termCompare id $ do - Refl <- testEquality sa4x sa4y - Refl <- testEquality sa3x sa3y - Refl <- testEquality sa2x sa2y - Refl <- testEquality sa1x sa1y - case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f a4x a3x a2x a1x)) of - Dict -> Just (compare x y) - --------------------------------------------------------------------------------- --- Generic - -type Eithers1 (f :: k1 -> Type) = - Eithers1' (EnumFromTo (MinBound :: k1) (MaxBound :: k1)) f - --- | TODO: Mak1e this logarithmic. -type family Eithers1' (xs :: [k1]) (f :: k1 -> Type) :: Type where - Eithers1' (x ': '[]) f = f x - Eithers1' (x ': xs) f = Either (f x) (Eithers1' xs f) - -instance forall k1 (f :: k1 -> Type) - . ( SingKind k1 - , PEnum ('Proxy :: Proxy k1) - , PBounded ('Proxy :: Proxy k1) - , G.Generic (DemoteRep k1) - , Dict1 G.Generic f - , Dict1 (Inj (Eithers1 f)) f - ) => G.Generic (Exinst.Some1 f) - where - type Rep (Exinst.Some1 (f :: k1 -> Type)) = - G.Rep (DemoteRep k1, Eithers1 f) - {-# INLINABLE from #-} - from = \s1x -> withSome1Sing s1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (G.Generic (f a1)) of - Dict -> case dict1 sa1 :: Dict (Inj (Eithers1 f) (f a1)) of - Dict -> G.from (fromSing sa1, inj x) - {-# INLINABLE to #-} - to = \(G.M1 (G.M1 (G.M1 (G.K1 da1) G.:*: G.M1 (G.K1 ex)))) -> - withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (Inj (Eithers1 f) (f a1)) of - Dict -> case prj ex of - Just x -> Exinst.Some1 sa1 (x :: f a1) - Nothing -> error "Generic Some1: Malformed Rep" - ---- -type Eithers2 (f :: k2 -> k1 -> Type) = - Eithers2' (Cartesian2 (EnumFromTo (MinBound :: k2) (MaxBound :: k2)) - (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f - --- | TODO: Mak1e this logarithmic. -type family Eithers2' (xs :: [(k2, k1)]) (f :: k2 -> k1 -> Type) :: Type where - Eithers2' ( '(x2, x1) ': '[]) f = f x2 x1 - Eithers2' ( '(x2, x1) ': xs) f = Either (f x2 x1) (Eithers2' xs f) - -type family Cartesian2 (xs2 :: [k2]) (xs1 :: [k1]) :: [(k2,k1)] where - Cartesian2 '[] xs1 = '[] - Cartesian2 (x2 ': xs2) xs1 = - List.Concat [List.Map (Tuple2Sym1 x2) xs1, Cartesian2 xs2 xs1] - - -instance forall k2 k1 (f :: k2 -> k1 -> Type) - . ( SingKind k2 - , SingKind k1 - , PEnum ('Proxy :: Proxy k2) - , PEnum ('Proxy :: Proxy k1) - , PBounded ('Proxy :: Proxy k2) - , PBounded ('Proxy :: Proxy k1) - , G.Generic (DemoteRep k2) - , G.Generic (DemoteRep k1) - , Dict2 G.Generic f - , Dict2 (Inj (Eithers2 f)) f - ) => G.Generic (Exinst.Some2 f) - where - type Rep (Exinst.Some2 (f :: k2 -> k1 -> Type)) = - G.Rep ((DemoteRep k2, DemoteRep k1), Eithers2 f) - {-# INLINABLE from #-} - from = \s2x -> withSome2Sing s2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (G.Generic (f a2 a1)) of - Dict -> case dict2 sa2 sa1 :: Dict (Inj (Eithers2 f) (f a2 a1)) of - Dict -> G.from ((fromSing sa2, fromSing sa1), inj x) - {-# INLINABLE to #-} - to = \(G.M1 (G.M1 (G.M1 (G.K1 (da2, da1)) G.:*: G.M1 (G.K1 ex)))) -> - withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (Inj (Eithers2 f) (f a2 a1)) of - Dict -> case prj ex of - Just x -> Exinst.Some2 sa2 sa1 (x :: f a2 a1) - Nothing -> error "Generic Some2: Malformed Rep" - - ---- -type Eithers3 (f :: k3 -> k2 -> k1 -> Type) = - Eithers3' (Cartesian3 (EnumFromTo (MinBound :: k3) (MaxBound :: k3)) - (EnumFromTo (MinBound :: k2) (MaxBound :: k2)) - (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f - --- | TODO: Mak1e this logarithmic. -type family Eithers3' (xs :: [(k3, (k2, k1))]) (f :: k3 -> k2 -> k1 -> Type) :: Type where - Eithers3' ( '(x3, '(x2, x1)) ': '[]) f = f x3 x2 x1 - Eithers3' ( '(x3, '(x2, x1)) ': xs) f = Either (f x3 x2 x1) (Eithers3' xs f) - --- | We use nested 2-tuples instead of 3-tuples because it's easier to implement. -type family Cartesian3 (xs3 :: [k3]) (xs2 :: [k2]) (xs1 :: [k1]) :: [(k3,(k2,k1))] where - Cartesian3 '[] xs2 xs1 = '[] - Cartesian3 (x3 ': xs3) xs2 xs1 = - List.Concat [ List.Map (Tuple2Sym1 x3) (Cartesian2 xs2 xs1) - , Cartesian3 xs3 xs2 xs1 ] - - -instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type) - . ( SingKind k3 - , SingKind k2 - , SingKind k1 - , PEnum ('Proxy :: Proxy k3) - , PEnum ('Proxy :: Proxy k2) - , PEnum ('Proxy :: Proxy k1) - , PBounded ('Proxy :: Proxy k3) - , PBounded ('Proxy :: Proxy k2) - , PBounded ('Proxy :: Proxy k1) - , G.Generic (DemoteRep k3) - , G.Generic (DemoteRep k2) - , G.Generic (DemoteRep k1) - , Dict3 G.Generic f - , Dict3 (Inj (Eithers3 f)) f - ) => G.Generic (Exinst.Some3 f) - where - type Rep (Exinst.Some3 (f :: k3 -> k2 -> k1 -> Type)) = - G.Rep ((DemoteRep k3, DemoteRep k2, DemoteRep k1), Eithers3 f) - {-# INLINABLE from #-} - from = \s3x -> withSome3Sing s3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (G.Generic (f a3 a2 a1)) of - Dict -> case dict3 sa3 sa2 sa1 :: Dict (Inj (Eithers3 f) (f a3 a2 a1)) of - Dict -> G.from ((fromSing sa3, fromSing sa2, fromSing sa1), inj x) - {-# INLINABLE to #-} - to = \(G.M1 (G.M1 (G.M1 (G.K1 (da3, da2, da1)) G.:*: G.M1 (G.K1 ex)))) -> - withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (Inj (Eithers3 f) (f a3 a2 a1)) of - Dict -> case prj ex of - Just x -> Exinst.Some3 sa3 sa2 sa1 (x :: f a3 a2 a1) - Nothing -> error "Generic Some3: Malformed Rep" - - ---- -type Eithers4 (f :: k4 -> k3 -> k2 -> k1 -> Type) = - Eithers4' (Cartesian4 (EnumFromTo (MinBound :: k4) (MaxBound :: k4)) - (EnumFromTo (MinBound :: k3) (MaxBound :: k3)) - (EnumFromTo (MinBound :: k2) (MaxBound :: k2)) - (EnumFromTo (MinBound :: k1) (MaxBound :: k1))) f - --- | TODO: Mak1e this logarithmic. -type family Eithers4' (xs :: [(k4, (k3, (k2, k1)))]) (f :: k4 -> k3 -> k2 -> k1 -> Type) :: Type where - Eithers4' ( '( x4, '(x3, '(x2, x1))) ': '[]) f = f x4 x3 x2 x1 - Eithers4' ( '( x4, '(x3, '(x2, x1))) ': xs) f = Either (f x4 x3 x2 x1) (Eithers4' xs f) - --- | We use nested 2-tuples instead of 4-tuples because it's easier to implement. -type family Cartesian4 (xs4 :: [k4]) (xs3 :: [k3]) (xs2 :: [k2]) (xs1 :: [k1]) :: [(k4,(k3,(k2,k1)))] where - Cartesian4 '[] xs3 xs2 xs1 = '[] - Cartesian4 (x4 ': xs4) xs3 xs2 xs1 = - List.Concat [ List.Map (Tuple2Sym1 x4) (Cartesian3 xs3 xs2 xs1) - , Cartesian4 xs4 xs3 xs2 xs1 ] - - -instance forall k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) - . ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , PEnum ('Proxy :: Proxy k4) - , PEnum ('Proxy :: Proxy k3) - , PEnum ('Proxy :: Proxy k2) - , PEnum ('Proxy :: Proxy k1) - , PBounded ('Proxy :: Proxy k4) - , PBounded ('Proxy :: Proxy k3) - , PBounded ('Proxy :: Proxy k2) - , PBounded ('Proxy :: Proxy k1) - , G.Generic (DemoteRep k4) - , G.Generic (DemoteRep k3) - , G.Generic (DemoteRep k2) - , G.Generic (DemoteRep k1) - , Dict4 G.Generic f - , Dict4 (Inj (Eithers4 f)) f - ) => G.Generic (Exinst.Some4 f) - where - type Rep (Exinst.Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type)) = - G.Rep ((DemoteRep k4, DemoteRep k3, DemoteRep k2, DemoteRep k1), Eithers4 f) - {-# INLINABLE from #-} - from = \s4x -> withSome4Sing s4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (G.Generic (f a4 a3 a2 a1)) of - Dict -> case dict4 sa4 sa3 sa2 sa1 :: Dict (Inj (Eithers4 f) (f a4 a3 a2 a1)) of - Dict -> G.from ((fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1), inj x) - {-# INLINABLE to #-} - to = \(G.M1 (G.M1 (G.M1 (G.K1 (da4, da3, da2, da1)) G.:*: G.M1 (G.K1 ex)))) -> - withSomeSing da4 $ \(sa4 :: Sing (a4 :: k4)) -> - withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Inj (Eithers4 f) (f a4 a3 a2 a1)) of - Dict -> case prj ex of - Just x -> Exinst.Some4 sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) - Nothing -> error "Generic Some4: Malformed Rep" - --------------------------------------------------------------------------------- --------------------------------------------------------------------------------- --- Out of the box 'DictX' instances for some @base@ types - -instance - (c 'False, c 'True - ) => Dict0 (c :: Bool -> Constraint) where - {-# INLINABLE dict0 #-} - dict0 = \case { SFalse -> Dict; STrue -> Dict } - -instance - ( c (f 'False), c (f 'True) - ) => Dict1 c (f :: Bool -> k0) where - {-# INLINABLE dict1 #-} - dict1 = \case { SFalse -> Dict; STrue -> Dict } - -instance - ( Dict1 c (f 'False), Dict1 c (f 'True) - ) => Dict2 c (f :: Bool -> k1 -> k0) where - {-# INLINABLE dict2 #-} - dict2 = \x -> case x of { SFalse -> dict1; STrue -> dict1 } - -instance - ( Dict2 c (f 'False), Dict2 c (f 'True) - ) => Dict3 c (f :: Bool -> k2 -> k1 -> k0) where - {-# INLINABLE dict3 #-} - dict3 = \x -> case x of { SFalse -> dict2; STrue -> dict2 } - -instance - ( Dict3 c (f 'False), Dict3 c (f 'True) - ) => Dict4 c (f :: Bool -> k3 -> k2 -> k1 -> k0) where - {-# INLINABLE dict4 #-} - dict4 = \x -> case x of { SFalse -> dict3; STrue -> dict3 } - --------------------------------------------------------------------------------- --------------------------------------------------------------------------------- --- Misc - -class Inj b a where - inj :: a -> b - prj :: b -> Maybe a -instance Inj a a where - {-# INLINE inj #-} - inj = id - {-# INLINE prj #-} - prj = Just -instance Inj (Either a b) a where - {-# INLINE inj #-} - inj = Left - {-# INLINE prj #-} - prj = either Just (const Nothing) --- | TODO: Make this logarithmic. -instance {-# OVERLAPPABLE #-} Inj x a => Inj (Either b x) a where - {-# INLINE inj #-} - inj = Right . inj - {-# INLINE prj #-} - prj = either (const Nothing) prj - diff --git a/src/lib/Exinst/Instances/Binary.hs b/src/lib/Exinst/Instances/Binary.hs deleted file mode 100644 --- a/src/lib/Exinst/Instances/Binary.hs +++ /dev/null @@ -1,137 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'Bin.Binary' instances for 'Some1', 'Some2', 'Some3' --- and 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', --- 'Dict3' and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.Binary () where - -import qualified Data.Binary as Bin -import Data.Constraint -import Data.Singletons -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k1 -> *). - ( SingKind k1 - , Bin.Binary (DemoteRep k1) - , Dict1 Bin.Binary f - ) => Bin.Binary (Some1 f) where - {-# INLINABLE put #-} - put = \some1x -> - withSome1Sing some1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (Bin.Binary (f a1)) of - Dict -> do - Bin.put (fromSing sa1) - Bin.put x - {-# INLINABLE get #-} - get = do - rsa1 <- Bin.get - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (Bin.Binary (f a1)) of - Dict -> do - x :: f a1 <- Bin.get - pure (Some1 sa1 x) - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k2 -> k1 -> *). - ( SingKind k2 - , SingKind k1 - , Bin.Binary (DemoteRep k2) - , Bin.Binary (DemoteRep k1) - , Dict2 Bin.Binary f - ) => Bin.Binary (Some2 f) where - {-# INLINABLE put #-} - put = \some2x -> - withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of - Dict -> do - Bin.put (fromSing sa2, fromSing sa1) - Bin.put x - {-# INLINABLE get #-} - get = do - (rsa2, rsa1) <- Bin.get - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (Bin.Binary (f a2 a1)) of - Dict -> do - x :: f a2 a1 <- Bin.get - pure (Some2 sa2 sa1 x) - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k3 -> k2 -> k1 -> *). - ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Bin.Binary (DemoteRep k3) - , Bin.Binary (DemoteRep k2) - , Bin.Binary (DemoteRep k1) - , Dict3 Bin.Binary f - ) => Bin.Binary (Some3 f) where - {-# INLINABLE put #-} - put = \some3x -> - withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of - Dict -> do - Bin.put (fromSing sa3, fromSing sa2, fromSing sa1) - Bin.put x - {-# INLINABLE get #-} - get = do - (rsa3, rsa2, rsa1) <- Bin.get - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (Bin.Binary (f a3 a2 a1)) of - Dict -> do - x :: f a3 a2 a1 <- Bin.get - pure (Some3 sa3 sa2 sa1 x) - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k4 -> k3 -> k2 -> k1 -> *). - ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Bin.Binary (DemoteRep k4) - , Bin.Binary (DemoteRep k3) - , Bin.Binary (DemoteRep k2) - , Bin.Binary (DemoteRep k1) - , Dict4 Bin.Binary f - ) => Bin.Binary (Some4 f) where - {-# INLINABLE put #-} - put = \some4x -> - withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Bin.Binary (f a4 a3 a2 a1)) of - Dict -> do - Bin.put (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1) - Bin.put x - {-# INLINABLE get #-} - get = do - (rsa4, rsa3, rsa2, rsa1) <- Bin.get - withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Bin.Binary (f a4 a3 a2 a1)) of - Dict -> do - x :: f a4 a3 a2 a1 <- Bin.get - pure (Some4 sa4 sa3 sa2 sa1 x) diff --git a/src/lib/Exinst/Instances/Bytes.hs b/src/lib/Exinst/Instances/Bytes.hs deleted file mode 100644 --- a/src/lib/Exinst/Instances/Bytes.hs +++ /dev/null @@ -1,138 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'By.Serial' instances for 'Some1', 'Some2', 'Some3' --- and 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', --- 'Dict3' and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.Bytes () where - -import qualified Data.Bytes.Serial as By -import Data.Constraint -import Data.Singletons -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - --- | Compatible with the 'Data.Binary.Binary' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k1 -> *). - ( SingKind k1 - , By.Serial (DemoteRep k1) - , Dict1 By.Serial f - ) => By.Serial (Some1 f) where - {-# INLINABLE serialize #-} - serialize = \some1x -> - withSome1Sing some1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (By.Serial (f a1)) of - Dict -> do - By.serialize (fromSing sa1) - By.serialize x - {-# INLINABLE deserialize #-} - deserialize = do - rsa1 <- By.deserialize - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (By.Serial (f a1)) of - Dict -> do - x :: f a1 <- By.deserialize - pure (Some1 sa1 x) - --- | Compatible with the 'Data.Binary.Binary' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k2 -> k1 -> *). - ( SingKind k2 - , SingKind k1 - , By.Serial (DemoteRep k2) - , By.Serial (DemoteRep k1) - , Dict2 By.Serial f - ) => By.Serial (Some2 f) where - {-# INLINABLE serialize #-} - serialize = \some2x -> - withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (By.Serial (f a2 a1)) of - Dict -> do - By.serialize (fromSing sa2, fromSing sa1) - By.serialize x - {-# INLINABLE deserialize #-} - deserialize = do - (rsa2, rsa1) <- By.deserialize - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (By.Serial (f a2 a1)) of - Dict -> do - x :: f a2 a1 <- By.deserialize - pure (Some2 sa2 sa1 x) - --- | Compatible with the 'Data.Binary.Binary' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k3 -> k2 -> k1 -> *). - ( SingKind k3 - , SingKind k2 - , SingKind k1 - , By.Serial (DemoteRep k3) - , By.Serial (DemoteRep k2) - , By.Serial (DemoteRep k1) - , Dict3 By.Serial f - ) => By.Serial (Some3 f) where - {-# INLINABLE serialize #-} - serialize = \some3x -> - withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f a3 a2 a1)) of - Dict -> do - By.serialize (fromSing sa3, fromSing sa2, fromSing sa1) - By.serialize x - {-# INLINABLE deserialize #-} - deserialize = do - (rsa3, rsa2, rsa1) <- By.deserialize - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f a3 a2 a1)) of - Dict -> do - x :: f a3 a2 a1 <- By.deserialize - pure (Some3 sa3 sa2 sa1 x) - --- | Compatible with the 'Data.Binary.Binary' instance and --- 'Data.Serialize.Serialize' instance, provided all of the 'DemoteRep's and the --- fully applied @f@ instances are compatible as well. -instance forall (f :: k4 -> k3 -> k2 -> k1 -> *). - ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , By.Serial (DemoteRep k4) - , By.Serial (DemoteRep k3) - , By.Serial (DemoteRep k2) - , By.Serial (DemoteRep k1) - , Dict4 By.Serial f - ) => By.Serial (Some4 f) where - {-# INLINABLE serialize #-} - serialize = \some4x -> - withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f a4 a3 a2 a1)) of - Dict -> do - By.serialize (fromSing sa4, fromSing sa3, - fromSing sa2, fromSing sa1) - By.serialize x - {-# INLINABLE deserialize #-} - deserialize = do - (rsa4, rsa3, rsa2, rsa1) <- By.deserialize - withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f a4 a3 a2 a1)) of - Dict -> do - x :: f a4 a3 a2 a1 <- By.deserialize - pure (Some4 sa4 sa3 sa2 sa1 x) diff --git a/src/lib/Exinst/Instances/Cereal.hs b/src/lib/Exinst/Instances/Cereal.hs deleted file mode 100644 --- a/src/lib/Exinst/Instances/Cereal.hs +++ /dev/null @@ -1,138 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'Cer.Serialize' instances for 'Some1', 'Some2', 'Some3' --- and 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', --- 'Dict3' and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.Cereal () where - -import qualified Data.Serialize as Cer -import Data.Constraint -import Data.Singletons -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Binary.Binary' instance, provided all of the 'DemoteRep's and the fully --- applied @f@ instances are compatible as well. -instance forall (f :: k1 -> *). - ( SingKind k1 - , Cer.Serialize (DemoteRep k1) - , Dict1 Cer.Serialize f - ) => Cer.Serialize (Some1 f) where - {-# INLINABLE put #-} - put = \some1x -> - withSome1Sing some1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (Cer.Serialize (f a1)) of - Dict -> do - Cer.put (fromSing sa1) - Cer.put x - {-# INLINABLE get #-} - get = do - rsa1 <- Cer.get - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (Cer.Serialize (f a1)) of - Dict -> do - x :: f a1 <- Cer.get - pure (Some1 sa1 x) - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Binary.Binary' instance, provided all of the 'DemoteRep's and the fully --- applied @f@ instances are compatible as well. -instance forall (f :: k2 -> k1 -> *). - ( SingKind k2 - , SingKind k1 - , Cer.Serialize (DemoteRep k2) - , Cer.Serialize (DemoteRep k1) - , Dict2 Cer.Serialize f - ) => Cer.Serialize (Some2 f) where - {-# INLINABLE put #-} - put = \some2x -> - withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (Cer.Serialize (f a2 a1)) of - Dict -> do - Cer.put (fromSing sa2, fromSing sa1) - Cer.put x - {-# INLINABLE get #-} - get = do - (rsa2, rsa1) <- Cer.get - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (Cer.Serialize (f a2 a1)) of - Dict -> do - x :: f a2 a1 <- Cer.get - pure (Some2 sa2 sa1 x) - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Binary.Binary' instance, provided all of the 'DemoteRep's and the fully --- applied @f@ instances are compatible as well. -instance forall (f :: k3 -> k2 -> k1 -> *). - ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Cer.Serialize (DemoteRep k3) - , Cer.Serialize (DemoteRep k2) - , Cer.Serialize (DemoteRep k1) - , Dict3 Cer.Serialize f - ) => Cer.Serialize (Some3 f) where - {-# INLINABLE put #-} - put = \some3x -> - withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a3 a2 a1)) of - Dict -> do - Cer.put (fromSing sa3, fromSing sa2, fromSing sa1) - Cer.put x - {-# INLINABLE get #-} - get = do - (rsa3, rsa2, rsa1) <- Cer.get - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a3 a2 a1)) of - Dict -> do - x :: f a3 a2 a1 <- Cer.get - pure (Some3 sa3 sa2 sa1 x) - --- | Compatible with the 'Data.Bytes.Serial.Serial' instance and --- 'Data.Binary.Binary' instance, provided all of the 'DemoteRep's and the fully --- applied @f@ instances are compatible as well. -instance forall (f :: k4 -> k3 -> k2 -> k1 -> *). - ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Cer.Serialize (DemoteRep k4) - , Cer.Serialize (DemoteRep k3) - , Cer.Serialize (DemoteRep k2) - , Cer.Serialize (DemoteRep k1) - , Dict4 Cer.Serialize f - ) => Cer.Serialize (Some4 f) where - {-# INLINABLE put #-} - put = \some4x -> - withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a4 a3 a2 a1)) of - Dict -> do - Cer.put (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1) - Cer.put x - {-# INLINABLE get #-} - get = do - (rsa4, rsa3, rsa2, rsa1) <- Cer.get - withSomeSing rsa4 $ \(sa4 :: Sing (a4 :: k4)) -> - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Cer.Serialize (f a4 a3 a2 a1)) of - Dict -> do - x :: f a4 a3 a2 a1 <- Cer.get - pure (Some4 sa4 sa3 sa2 sa1 x) - diff --git a/src/lib/Exinst/Instances/DeepSeq.hs b/src/lib/Exinst/Instances/DeepSeq.hs deleted file mode 100644 --- a/src/lib/Exinst/Instances/DeepSeq.hs +++ /dev/null @@ -1,60 +0,0 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'NFData' instances for 'Some1', 'Some2', 'Some3' and --- 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', 'Dict3' --- and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.DeepSeq () where - -import Control.DeepSeq (NFData(rnf)) -import Data.Constraint -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - -instance forall (f :: k1 -> *). - ( Dict1 NFData f - ) => NFData (Some1 f) where - {-# INLINABLE rnf #-} - rnf = \(!some1x) -> - withSome1Sing some1x $ \ !sa1 !(x :: f a1) -> - case dict1 sa1 :: Dict (NFData (f a1)) of - Dict -> rnf x `seq` () - -instance forall (f :: k2 -> k1 -> *). - ( Dict2 NFData f - ) => NFData (Some2 f) where - {-# INLINABLE rnf #-} - rnf = \(!some2x) -> - withSome2Sing some2x $ \ !sa2 !sa1 !(x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (NFData (f a2 a1)) of - Dict -> rnf x `seq` () - -instance forall (f :: k3 -> k2 -> k1 -> *). - ( Dict3 NFData f - ) => NFData (Some3 f) where - {-# INLINABLE rnf #-} - rnf = \(!some3x) -> - withSome3Sing some3x $ \ !sa3 !sa2 !sa1 !(x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (NFData (f a3 a2 a1)) of - Dict -> rnf x `seq` () - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> *). - ( Dict4 NFData f - ) => NFData (Some4 f) where - {-# INLINABLE rnf #-} - rnf = \(!some4x) -> - withSome4Sing some4x $ \ !(sa4) !sa3 !sa2 !sa1 !(x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (NFData (f a4 a3 a2 a1)) of - Dict -> rnf x `seq` () - diff --git a/src/lib/Exinst/Instances/Hashable.hs b/src/lib/Exinst/Instances/Hashable.hs deleted file mode 100644 --- a/src/lib/Exinst/Instances/Hashable.hs +++ /dev/null @@ -1,99 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'Hashable' instances for 'Some1', 'Some2', 'Some3' and --- 'Some4' from "Exinst", provided situable 'Dict1', 'Dict2', 'Dict3' --- and 'Dict4' instances are available. --- --- See the README file in the @exinst@ package for more general documentation: --- https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.Hashable () where - -import Data.Hashable (Hashable(hashWithSalt)) -import Data.Constraint -import Data.Singletons -import Prelude - -import Exinst.Internal - --------------------------------------------------------------------------------- - --- | Some salt we add to hashes calculated in this module. -salt0 :: Int -salt0 = 6700417 - --------------------------------------------------------------------------------- - -instance forall (f :: k1 -> *) - . ( SingKind k1 - , Hashable (DemoteRep k1) - , Dict1 Hashable f - ) => Hashable (Some1 f) - where - {-# INLINABLE hashWithSalt #-} - hashWithSalt salt some1x = withSome1Sing some1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (Hashable (f a1)) of - Dict -> salt `hashWithSalt` salt0 - `hashWithSalt` fromSing sa1 - `hashWithSalt` x - -instance forall (f :: k2 -> k1 -> *) - . ( SingKind k2 - , SingKind k1 - , Hashable (DemoteRep k2) - , Hashable (DemoteRep k1) - , Dict2 Hashable f - ) => Hashable (Some2 f) - where - {-# INLINABLE hashWithSalt #-} - hashWithSalt salt some2x = withSome2Sing some2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (Hashable (f a2 a1)) of - Dict -> salt `hashWithSalt` salt0 - `hashWithSalt` fromSing sa2 - `hashWithSalt` fromSing sa1 - `hashWithSalt` x - -instance forall (f :: k3 -> k2 -> k1 -> *) - . ( SingKind k3 - , SingKind k2 - , SingKind k1 - , Hashable (DemoteRep k3) - , Hashable (DemoteRep k2) - , Hashable (DemoteRep k1) - , Dict3 Hashable f - ) => Hashable (Some3 f) - where - {-# INLINABLE hashWithSalt #-} - hashWithSalt salt some3x = withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Hashable (f a3 a2 a1)) of - Dict -> salt `hashWithSalt` salt0 - `hashWithSalt` fromSing sa3 - `hashWithSalt` fromSing sa2 - `hashWithSalt` fromSing sa1 - `hashWithSalt` x - -instance forall (f :: k4 -> k3 -> k2 -> k1 -> *) - . ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , Hashable (DemoteRep k4) - , Hashable (DemoteRep k3) - , Hashable (DemoteRep k2) - , Hashable (DemoteRep k1) - , Dict4 Hashable f - ) => Hashable (Some4 f) - where - {-# INLINABLE hashWithSalt #-} - hashWithSalt salt some4x = withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Hashable (f a4 a3 a2 a1)) of - Dict -> salt `hashWithSalt` salt0 - `hashWithSalt` fromSing sa4 - `hashWithSalt` fromSing sa3 - `hashWithSalt` fromSing sa2 - `hashWithSalt` fromSing sa1 - `hashWithSalt` x diff --git a/src/lib/Exinst/Instances/QuickCheck.hs b/src/lib/Exinst/Instances/QuickCheck.hs deleted file mode 100644 --- a/src/lib/Exinst/Instances/QuickCheck.hs +++ /dev/null @@ -1,106 +0,0 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeInType #-} - -{-# OPTIONS_GHC -fno-warn-orphans #-} - --- | This module exports 'QC.arbitrary' instances for 'Exinst.Some1', 'Some2', --- 'Some3' and 'Some4' from "Exinst", provided situable 'Dict1', --- 'Dict2', 'Dict3' and 'Dict4' instances are available. --- --- See the README file for more general documentation: https://hackage.haskell.org/package/exinst#readme -module Exinst.Instances.QuickCheck () where - -import Data.Constraint -import Data.Kind (Type) -import Data.Singletons (SingKind, Sing, DemoteRep, withSomeSing) -import qualified Test.QuickCheck as QC - -import Exinst.Internal - --------------------------------------------------------------------------------- - -instance - forall k1 (f :: k1 -> Type). - ( SingKind k1 - , QC.Arbitrary (DemoteRep k1) - , Dict1 QC.Arbitrary f - ) => QC.Arbitrary (Some1 f) where - arbitrary = do - da1 <- QC.arbitrary - withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict1 sa1 :: Dict (QC.Arbitrary (f a1)) of - Dict -> Some1 sa1 <$> QC.arbitrary - shrink = \s1x -> withSome1Sing s1x $ \sa1 (x :: f a1) -> - case dict1 sa1 :: Dict (QC.Arbitrary (f a1)) of - Dict -> Some1 sa1 <$> QC.shrink x - -instance - forall k2 k1 (f :: k2 -> k1 -> Type). - ( SingKind k2 - , SingKind k1 - , QC.Arbitrary (DemoteRep k2) - , QC.Arbitrary (DemoteRep k1) - , Dict2 QC.Arbitrary f - ) => QC.Arbitrary (Some2 f) where - arbitrary = do - da2 <- QC.arbitrary - da1 <- QC.arbitrary - withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict2 sa2 sa1 :: Dict (QC.Arbitrary (f a2 a1)) of - Dict -> Some2 sa2 sa1 <$> QC.arbitrary - shrink = \s2x -> withSome2Sing s2x $ \sa2 sa1 (x :: f a2 a1) -> - case dict2 sa2 sa1 :: Dict (QC.Arbitrary (f a2 a1)) of - Dict -> Some2 sa2 sa1 <$> QC.shrink x - -instance - forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type). - ( SingKind k3 - , SingKind k2 - , SingKind k1 - , QC.Arbitrary (DemoteRep k3) - , QC.Arbitrary (DemoteRep k2) - , QC.Arbitrary (DemoteRep k1) - , Dict3 QC.Arbitrary f - ) => QC.Arbitrary (Some3 f) where - arbitrary = do - da3 <- QC.arbitrary - da2 <- QC.arbitrary - da1 <- QC.arbitrary - withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict3 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a3 a2 a1)) of - Dict -> Some3 sa3 sa2 sa1 <$> QC.arbitrary - shrink = \s3x -> withSome3Sing s3x $ \sa3 sa2 sa1 (x :: f a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a3 a2 a1)) of - Dict -> Some3 sa3 sa2 sa1 <$> QC.shrink x - -instance - forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type). - ( SingKind k4 - , SingKind k3 - , SingKind k2 - , SingKind k1 - , QC.Arbitrary (DemoteRep k4) - , QC.Arbitrary (DemoteRep k3) - , QC.Arbitrary (DemoteRep k2) - , QC.Arbitrary (DemoteRep k1) - , Dict4 QC.Arbitrary f - ) => QC.Arbitrary (Some4 f) where - arbitrary = do - da4 <- QC.arbitrary - da3 <- QC.arbitrary - da2 <- QC.arbitrary - da1 <- QC.arbitrary - withSomeSing da4 $ \(sa4 :: Sing (a4 :: k4)) -> - withSomeSing da3 $ \(sa3 :: Sing (a3 :: k3)) -> - withSomeSing da2 $ \(sa2 :: Sing (a2 :: k2)) -> - withSomeSing da1 $ \(sa1 :: Sing (a1 :: k1)) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a4 a3 a2 a1)) of - Dict -> Some4 sa4 sa3 sa2 sa1 <$> QC.arbitrary - shrink = \s3x -> withSome4Sing s3x $ \sa4 sa3 sa2 sa1 (x :: f a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (QC.Arbitrary (f a4 a3 a2 a1)) of - Dict -> Some4 sa4 sa3 sa2 sa1 <$> QC.shrink x - diff --git a/src/lib/Exinst/Internal.hs b/src/lib/Exinst/Internal.hs deleted file mode 100644 --- a/src/lib/Exinst/Internal.hs +++ /dev/null @@ -1,361 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE ExistentialQuantification #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} - - -module Exinst.Internal - ( -- * 1 type index - Some1(Some1) - , some1 - , fromSome1 - , _Some1 - , withSome1 - , withSome1Sing - , some1SingRep - , Dict1(dict1) - - -- * 2 type indexes - , Some2(Some2) - , some2 - , fromSome2 - , _Some2 - , withSome2 - , withSome2Sing - , some2SingRep - , Dict2(dict2) - - -- * 3 type indexes - , Some3(Some3) - , some3 - , fromSome3 - , _Some3 - , withSome3 - , withSome3Sing - , some3SingRep - , Dict3(dict3) - - -- * 4 type indexes - , Some4(Some4) - , some4 - , fromSome4 - , _Some4 - , withSome4 - , withSome4Sing - , some4SingRep - , Dict4(dict4) - - -- * Miscellaneous - , Dict0(dict0) - ) where - -import Data.Constraint -import Data.Kind (Type) -import Data.Profunctor (dimap, Choice(right')) -import Data.Singletons -import Data.Singletons.Decide -import Data.Type.Equality -import Prelude - --------------------------------------------------------------------------------- - -data Some1 (f1 :: k1 -> Type) = forall a1. - Some1 !(Sing a1) !(f1 a1) - -data Some2 (f2 :: k2 -> k1 -> Type) = forall a2 a1. - Some2 !(Sing a2) !(Sing a1) !(f2 a2 a1) - -data Some3 (f3 :: k3 -> k2 -> k1 -> Type) = forall a3 a2 a1. - Some3 !(Sing a3) !(Sing a2) !(Sing a1) !(f3 a3 a2 a1) - -data Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) = forall a4 a3 a2 a1. - Some4 !(Sing a4) !(Sing a3) !(Sing a2) !(Sing a1) !(f4 a4 a3 a2 a1) - --------------------------------------------------------------------------------- - -some1 - :: forall (f1 :: k1 -> Type) a1 - . SingI a1 - => f1 a1 - -> Some1 f1 -- ^ -some1 = Some1 (sing :: Sing a1) -{-# INLINE some1 #-} - -some2 - :: forall (f2 :: k2 -> k1 -> Type) a2 a1 - . (SingI a2, SingI a1) - => f2 a2 a1 - -> Some2 f2 -- ^ -some2 = Some2 (sing :: Sing a2) (sing :: Sing a1) -{-# INLINE some2 #-} - -some3 - :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1 - . (SingI a3, SingI a2, SingI a1) - => f3 a3 a2 a1 - -> Some3 f3 -- ^ -some3 = Some3 (sing :: Sing a3) (sing :: Sing a2) (sing :: Sing a1) -{-# INLINE some3 #-} - -some4 - :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1 - . (SingI a4, SingI a3, SingI a2, SingI a1) - => f4 a4 a3 a2 a1 - -> Some4 f4 -- ^ -some4 = Some4 (sing :: Sing a4) (sing :: Sing a3) - (sing :: Sing a2) (sing :: Sing a1) -{-# INLINE some4 #-} - --------------------------------------------------------------------------------- - -withSome1 - :: forall (f1 :: k1 -> Type) (r :: Type) - . Some1 f1 - -> (forall a1. SingI a1 => f1 a1 -> r) - -> r -- ^ -withSome1 s1 g = withSome1Sing s1 (\_ -> g) -{-# INLINABLE withSome1 #-} - -withSome2 - :: forall (f2 :: k2 -> k1 -> Type) (r :: Type) - . Some2 f2 - -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r) - -> r -- ^ -withSome2 s2 g = withSome2Sing s2 (\_ _ -> g) -{-# INLINABLE withSome2 #-} - -withSome3 - :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type) - . Some3 f3 - -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r) - -> r -- ^ -withSome3 s3 g = withSome3Sing s3 (\_ _ _ -> g) -{-# INLINABLE withSome3 #-} - -withSome4 - :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type) - . Some4 f4 - -> (forall a4 a3 a2 a1 - . (SingI a4, SingI a3, SingI a2, SingI a1) - => f4 a4 a3 a2 a1 -> r) - -> r -- ^ -withSome4 s4 g = withSome4Sing s4 (\_ _ _ _ -> g) -{-# INLINABLE withSome4 #-} - --------------------------------------------------------------------------------- - --- | Like 'withSome1', but takes an explicit 'Sing' besides the 'SingI' instance. -withSome1Sing - :: forall (f1 :: k1 -> Type) (r :: Type) - . Some1 f1 - -> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r) - -> r -- ^ -withSome1Sing (Some1 sa1 x) g = withSingI sa1 (g sa1 x) -{-# INLINABLE withSome1Sing #-} - --- | Like 'withSome2', but takes explicit 'Sing's besides the 'SingI' instances. -withSome2Sing - :: forall (f2 :: k2 -> k1 -> Type) (r :: Type) - . Some2 f2 - -> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r) - -> r -- ^ -withSome2Sing (Some2 sa2 sa1 x) g = withSingI sa2 (withSingI sa1 (g sa2 sa1 x)) -{-# INLINABLE withSome2Sing #-} - --- | Like 'withSome3', but takes explicit 'Sing's besides the 'SingI' instances. -withSome3Sing - :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type) - . Some3 f3 - -> (forall a3 a2 a1 - . (SingI a3, SingI a2, SingI a1) - => Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r) - -> r -- ^ -withSome3Sing (Some3 sa3 sa2 sa1 x) g = - withSingI sa3 (withSingI sa2 (withSingI sa1 (g sa3 sa2 sa1 x))) -{-# INLINABLE withSome3Sing #-} - --- | Like 'withSome4', but takes explicit 'Sing's besides the 'SingI' instances. -withSome4Sing - :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type) - . Some4 f4 - -> (forall a4 a3 a2 a1 - . (SingI a4, SingI a3, SingI a2, SingI a1) - => Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r) - -> r -- ^ -withSome4Sing (Some4 sa4 sa3 sa2 sa1 x) g = - withSingI sa4 (withSingI sa3 (withSingI sa2 (withSingI sa1 - (g sa4 sa3 sa2 sa1 x)))) -{-# INLINABLE withSome4Sing #-} - --------------------------------------------------------------------------------- - -fromSome1 - :: forall (f1 :: k1 -> Type) a1 - . (SingI a1, SDecide k1) - => Some1 f1 - -> Maybe (f1 a1) -- ^ -fromSome1 = \(Some1 sa1' x) -> do - Refl <- testEquality sa1' (sing :: Sing a1) - return x -{-# INLINABLE fromSome1 #-} - -fromSome2 - :: forall (f2 :: k2 -> k1 -> Type) a2 a1 - . ( SingI a2, SDecide k2 - , SingI a1, SDecide k1 ) - => Some2 f2 - -> Maybe (f2 a2 a1) -- ^ -fromSome2 = \(Some2 sa2' sa1' x) -> do - Refl <- testEquality sa2' (sing :: Sing a2) - Refl <- testEquality sa1' (sing :: Sing a1) - return x -{-# INLINABLE fromSome2 #-} - -fromSome3 - :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1 - . ( SingI a3, SDecide k3 - , SingI a2, SDecide k2 - , SingI a1, SDecide k1 ) - => Some3 f3 - -> Maybe (f3 a3 a2 a1) -- ^ -fromSome3 = \(Some3 sa3' sa2' sa1' x) -> do - Refl <- testEquality sa3' (sing :: Sing a3) - Refl <- testEquality sa2' (sing :: Sing a2) - Refl <- testEquality sa1' (sing :: Sing a1) - return x -{-# INLINABLE fromSome3 #-} - -fromSome4 - :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1 - . ( SingI a4, SDecide k4 - , SingI a3, SDecide k3 - , SingI a2, SDecide k2 - , SingI a1, SDecide k1 ) - => Some4 f4 - -> Maybe (f4 a4 a3 a2 a1) -- ^ -fromSome4 = \(Some4 sa4' sa3' sa2' sa1' x) -> do - Refl <- testEquality sa4' (sing :: Sing a4) - Refl <- testEquality sa3' (sing :: Sing a3) - Refl <- testEquality sa2' (sing :: Sing a2) - Refl <- testEquality sa1' (sing :: Sing a1) - return x -{-# INLINABLE fromSome4 #-} - --------------------------------------------------------------------------------- - --- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some1'. -_Some1 - :: forall (f1 :: k1 -> Type) a1 - . (SingI a1, SDecide k1) - => Prism' (Some1 f1) (f1 a1) -_Some1 = prism' some1 fromSome1 -{-# INLINE _Some1 #-} - --- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some2'. -_Some2 - :: forall (f2 :: k2 -> k1 -> Type) a2 a1 - . ( SingI a2, SDecide k2 - , SingI a1, SDecide k1 ) - => Prism' (Some2 f2) (f2 a2 a1) -_Some2 = prism' some2 fromSome2 -{-# INLINE _Some2 #-} - --- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some3'. -_Some3 - :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1 - . ( SingI a3, SDecide k3 - , SingI a2, SDecide k2 - , SingI a1, SDecide k1 ) - => Prism' (Some3 f3) (f3 a3 a2 a1) -_Some3 = prism' some3 fromSome3 -{-# INLINE _Some3 #-} - --- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some4'. -_Some4 - :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1 - . ( SingI a4, SDecide k4 - , SingI a3, SDecide k3 - , SingI a2, SDecide k2 - , SingI a1, SDecide k1 ) - => Prism' (Some4 f4) (f4 a4 a3 a2 a1) -_Some4 = prism' some4 fromSome4 -{-# INLINE _Some4 #-} - --------------------------------------------------------------------------------- - -some1SingRep - :: SingKind k1 - => Some1 (f1 :: k1 -> Type) - -> DemoteRep k1 -- ^ -some1SingRep = \(Some1 sa1 _) -> fromSing sa1 -{-# INLINE some1SingRep #-} - -some2SingRep - :: (SingKind k2, SingKind k1) - => Some2 (f2 :: k2 -> k1 -> Type) - -> (DemoteRep k2, DemoteRep k1) -- ^ -some2SingRep = \(Some2 sa2 sa1 _) -> (fromSing sa2, fromSing sa1) -{-# INLINE some2SingRep #-} - -some3SingRep - :: (SingKind k3, SingKind k2, SingKind k1) - => Some3 (f3 :: k3 -> k2 -> k1 -> Type) - -> (DemoteRep k3, DemoteRep k2, DemoteRep k1) -- ^ -some3SingRep = \(Some3 sa3 sa2 sa1 _) -> - (fromSing sa3, fromSing sa2, fromSing sa1) -{-# INLINE some3SingRep #-} - -some4SingRep - :: (SingKind k4, SingKind k3, SingKind k2, SingKind k1) - => Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) - -> (DemoteRep k4, DemoteRep k3, DemoteRep k2, DemoteRep k1) -- ^ -some4SingRep = \(Some4 sa4 sa3 sa2 sa1 _) -> - (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1) -{-# INLINE some4SingRep #-} - --------------------------------------------------------------------------------- - --- | 'Dict0' is a bit different from 'Dict1', 'Dict2', etc. in that it looks up --- an instance for the singleton type itself, and not for some other type --- indexed by said singleton type. -class Dict0 (c :: k0 -> Constraint) where - -- | Runtime lookup of the @c a0@ instance. - dict0 :: Sing a0 -> Dict (c a0) - -class Dict1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) where - -- | Runtime lookup of the @c (f1 a1)@ instance. - dict1 :: Sing a1 -> Dict (c (f1 a1)) - -class Dict2 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0) where - -- Runtime lookup of the @c (f2 a2 a1)@ instance. - dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1)) - -class Dict3 (c :: k0 -> Constraint) (f3 :: k3 -> k2 -> k1 -> k0) where - -- Runtime lookup of the @c (f3 a3 a2 a1)@ instance. - dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1)) - -class Dict4 (c :: k0 -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> k0) where - -- Runtime lookup of the @c (f4 a4 a3 a2 a1)@ instance. - dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1)) - --------------------------------------------------------------------------------- --- Miscelaneous @lens@-compatible stuff. - -type Prism s t a b - = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t) - -type Prism' s a = Prism s s a a - -prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b -prism bt seta = dimap seta (either pure (fmap bt)) . right' -{-# INLINE prism #-} - -prism' :: (b -> s) -> (s -> Maybe a) -> Prism s s a b -prism' bs sma = prism bs (\s -> maybe (Left s) Right (sma s)) -{-# INLINE prism' #-} - diff --git a/src/lib/Exinst/Internal/Product.hs b/src/lib/Exinst/Internal/Product.hs deleted file mode 100644 --- a/src/lib/Exinst/Internal/Product.hs +++ /dev/null @@ -1,139 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE PolyKinds #-} - -module Exinst.Internal.Product - ( P1(P1) - , P2(P2) - , P3(P3) - , P4(P4) - ) where - -import GHC.Generics (Generic) - -#ifdef VERSION_aeson -import Data.Aeson (FromJSON, ToJSON) -#endif - -#ifdef VERSION_binary -import qualified Data.Binary as Bin -#endif - -#ifdef VERSION_bytes -import qualified Data.Bytes.Serial as By -#endif - -#ifdef VERSION_cereal -import qualified Data.Serialize as Cer -#endif - -#ifdef VERSION_deepseq -import Control.DeepSeq (NFData) -#endif - -#ifdef VERSION_hashable -import Data.Hashable (Hashable) -#endif - -#ifdef VERSION_QuickCheck -import qualified Test.QuickCheck as QC -#endif - --------------------------------------------------------------------------------- --- Products - --- | Like 'Data.Functor.Product.Product' from "Data.Functor.Product", but --- only intended to be used with kinds other than 'Type'. --- --- This type is particularly useful when used in combination with 'Exinst.Some1' --- as @'Exinst.Some1' ('P1' l r)@, so as to ensure that @l@ and @r@ are indexed --- by the same type. Moreover, 'P1' already supports many common instances from --- @base@, @hashable@, @deepseq@, @aeson@, @bytes@, @cereal@, @binary@, and --- @quickcheck@ out of the box, so you can benefit from them as well. -data P1 l r (a1 :: k1) - = P1 (l a1) (r a1) - deriving (Eq, Show, Read, Ord, Generic) - --- | Like 'P1', but for @l@ and @r@ taking two type indexes. -data P2 l r (a2 :: k2) (a1 :: k1) - = P2 (l a2 a1) (r a2 a1) - deriving (Eq, Show, Read, Ord, Generic) - --- | Like 'P1', but for @l@ and @r@ taking three type indexes. -data P3 l r (a3 :: k3) (a2 :: k2) (a1 :: k1) - = P3 (l a3 a2 a1) (r a3 a2 a1) - deriving (Eq, Show, Read, Ord, Generic) - --- | Like 'P1', but for @l@ and @r@ taking four type indexes. -data P4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1) - = P4 (l a4 a3 a2 a1) (r a4 a3 a2 a1) - deriving (Eq, Show, Read, Ord, Generic) - --------------------------------------------------------------------------------- -#ifdef VERSION_hashable -instance (Hashable (l a1), Hashable (r a1)) => Hashable (P1 l r a1) -instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (P2 l r a2 a1) -instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (P3 l r a3 a2 a1) -instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (P4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef VERSION_deepseq -instance (NFData (l a1), NFData (r a1)) => NFData (P1 l r a1) -instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (P2 l r a2 a1) -instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (P3 l r a3 a2 a1) -instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (P4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef VERSION_aeson -instance (FromJSON (l a1), FromJSON (r a1)) => FromJSON (P1 l r a1) -instance (FromJSON (l a2 a1), FromJSON (r a2 a1)) => FromJSON (P2 l r a2 a1) -instance (FromJSON (l a3 a2 a1), FromJSON (r a3 a2 a1)) => FromJSON (P3 l r a3 a2 a1) -instance (FromJSON (l a4 a3 a2 a1), FromJSON (r a4 a3 a2 a1)) => FromJSON (P4 l r a4 a3 a2 a1) - -instance (ToJSON (l a1), ToJSON (r a1)) => ToJSON (P1 l r a1) -instance (ToJSON (l a2 a1), ToJSON (r a2 a1)) => ToJSON (P2 l r a2 a1) -instance (ToJSON (l a3 a2 a1), ToJSON (r a3 a2 a1)) => ToJSON (P3 l r a3 a2 a1) -instance (ToJSON (l a4 a3 a2 a1), ToJSON (r a4 a3 a2 a1)) => ToJSON (P4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef VERSION_bytes -instance (By.Serial (l a1), By.Serial (r a1)) => By.Serial (P1 l r a1) -instance (By.Serial (l a2 a1), By.Serial (r a2 a1)) => By.Serial (P2 l r a2 a1) -instance (By.Serial (l a3 a2 a1), By.Serial (r a3 a2 a1)) => By.Serial (P3 l r a3 a2 a1) -instance (By.Serial (l a4 a3 a2 a1), By.Serial (r a4 a3 a2 a1)) => By.Serial (P4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef VERSION_cereal -instance (Cer.Serialize (l a1), Cer.Serialize (r a1)) => Cer.Serialize (P1 l r a1) -instance (Cer.Serialize (l a2 a1), Cer.Serialize (r a2 a1)) => Cer.Serialize (P2 l r a2 a1) -instance (Cer.Serialize (l a3 a2 a1), Cer.Serialize (r a3 a2 a1)) => Cer.Serialize (P3 l r a3 a2 a1) -instance (Cer.Serialize (l a4 a3 a2 a1), Cer.Serialize (r a4 a3 a2 a1)) => Cer.Serialize (P4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef VERSION_binary -instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (P1 l r a1) -instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (P2 l r a2 a1) -instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (P3 l r a3 a2 a1) -instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (P4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef VERSION_QuickCheck -instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (P1 l r a1) where - arbitrary = P1 <$> QC.arbitrary <*> QC.arbitrary - shrink (P1 x y) = P1 <$> QC.shrink x <*> QC.shrink y -instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (P2 l r a2 a1) where - arbitrary = P2 <$> QC.arbitrary <*> QC.arbitrary - shrink (P2 x y) = P2 <$> QC.shrink x <*> QC.shrink y -instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (P3 l r a3 a2 a1) where - arbitrary = P3 <$> QC.arbitrary <*> QC.arbitrary - shrink (P3 x y) = P3 <$> QC.shrink x <*> QC.shrink y -instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (P4 l r a4 a3 a2 a1) where - arbitrary = P4 <$> QC.arbitrary <*> QC.arbitrary - shrink (P4 x y) = P4 <$> QC.shrink x <*> QC.shrink y -#endif diff --git a/src/lib/Exinst/Internal/Sum.hs b/src/lib/Exinst/Internal/Sum.hs deleted file mode 100644 --- a/src/lib/Exinst/Internal/Sum.hs +++ /dev/null @@ -1,143 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE PolyKinds #-} - -module Exinst.Internal.Sum - ( S1(S1L,S1R) - , S2(S2L,S2R) - , S3(S3L,S3R) - , S4(S4L,S4R) - ) where - -import GHC.Generics (Generic) - -#ifdef VERSION_aeson -import Data.Aeson (FromJSON, ToJSON) -#endif - -#ifdef VERSION_binary -import qualified Data.Binary as Bin -#endif - -#ifdef VERSION_bytes -import qualified Data.Bytes.Serial as By -#endif - -#ifdef VERSION_cereal -import qualified Data.Serialize as Cer -#endif - -#ifdef VERSION_deepseq -import Control.DeepSeq (NFData) -#endif - -#ifdef VERSION_hashable -import Data.Hashable (Hashable) -#endif - -#ifdef VERSION_QuickCheck -import qualified Test.QuickCheck as QC -#endif - --------------------------------------------------------------------------------- --- Sums - --- | Like 'Data.Functor.Sum.Sum' from "Data.Functor.Sum", but --- only intended to be used with kinds other than 'Type'. --- --- This type is particularly useful when used in combination with 'Exinst.Some1' --- as @'Exinst.Some1' ('S1' l r)@, so as to ensure that @l@ and @r@ are indexed --- by the same type. Moreover, 'S1' already supports many common instances from --- @base@, @hashable@, @deepseq@, @aeson@, @bytes@, @cereal@, @binary@, and --- @quickcheck@ out of the box, so you can benefit from them as well. -data S1 l r (a1 :: k1) - = S1L (l a1) | S1R (r a1) - deriving (Eq, Show, Read, Ord, Generic) - --- | Like 'S1', but for @l@ and @r@ taking two type indexes. -data S2 l r (a2 :: k2) (a1 :: k1) - = S2L (l a2 a1) | S2R (r a2 a1) - deriving (Eq, Show, Read, Ord, Generic) - --- | Like 'S1', but for @l@ and @r@ taking three type indexes. -data S3 l r (a3 :: k3) (a2 :: k2) (a1 :: k1) - = S3L (l a3 a2 a1) | S3R (r a3 a2 a1) - deriving (Eq, Show, Read, Ord, Generic) - --- | Like 'S1', but for @l@ and @r@ taking four type indexes. -data S4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1) - = S4L (l a4 a3 a2 a1) | S4R (r a4 a3 a2 a1) - deriving (Eq, Show, Read, Ord, Generic) - --------------------------------------------------------------------------------- -#ifdef VERSION_hashable -instance (Hashable (l a1), Hashable (r a1)) => Hashable (S1 l r a1) -instance (Hashable (l a2 a1), Hashable (r a2 a1)) => Hashable (S2 l r a2 a1) -instance (Hashable (l a3 a2 a1), Hashable (r a3 a2 a1)) => Hashable (S3 l r a3 a2 a1) -instance (Hashable (l a4 a3 a2 a1), Hashable (r a4 a3 a2 a1)) => Hashable (S4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef VERSION_deepseq -instance (NFData (l a1), NFData (r a1)) => NFData (S1 l r a1) -instance (NFData (l a2 a1), NFData (r a2 a1)) => NFData (S2 l r a2 a1) -instance (NFData (l a3 a2 a1), NFData (r a3 a2 a1)) => NFData (S3 l r a3 a2 a1) -instance (NFData (l a4 a3 a2 a1), NFData (r a4 a3 a2 a1)) => NFData (S4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef VERSION_aeson -instance (FromJSON (l a1), FromJSON (r a1)) => FromJSON (S1 l r a1) -instance (FromJSON (l a2 a1), FromJSON (r a2 a1)) => FromJSON (S2 l r a2 a1) -instance (FromJSON (l a3 a2 a1), FromJSON (r a3 a2 a1)) => FromJSON (S3 l r a3 a2 a1) -instance (FromJSON (l a4 a3 a2 a1), FromJSON (r a4 a3 a2 a1)) => FromJSON (S4 l r a4 a3 a2 a1) - -instance (ToJSON (l a1), ToJSON (r a1)) => ToJSON (S1 l r a1) -instance (ToJSON (l a2 a1), ToJSON (r a2 a1)) => ToJSON (S2 l r a2 a1) -instance (ToJSON (l a3 a2 a1), ToJSON (r a3 a2 a1)) => ToJSON (S3 l r a3 a2 a1) -instance (ToJSON (l a4 a3 a2 a1), ToJSON (r a4 a3 a2 a1)) => ToJSON (S4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef VERSION_bytes -instance (By.Serial (l a1), By.Serial (r a1)) => By.Serial (S1 l r a1) -instance (By.Serial (l a2 a1), By.Serial (r a2 a1)) => By.Serial (S2 l r a2 a1) -instance (By.Serial (l a3 a2 a1), By.Serial (r a3 a2 a1)) => By.Serial (S3 l r a3 a2 a1) -instance (By.Serial (l a4 a3 a2 a1), By.Serial (r a4 a3 a2 a1)) => By.Serial (S4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef VERSION_cereal -instance (Cer.Serialize (l a1), Cer.Serialize (r a1)) => Cer.Serialize (S1 l r a1) -instance (Cer.Serialize (l a2 a1), Cer.Serialize (r a2 a1)) => Cer.Serialize (S2 l r a2 a1) -instance (Cer.Serialize (l a3 a2 a1), Cer.Serialize (r a3 a2 a1)) => Cer.Serialize (S3 l r a3 a2 a1) -instance (Cer.Serialize (l a4 a3 a2 a1), Cer.Serialize (r a4 a3 a2 a1)) => Cer.Serialize (S4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef VERSION_binary -instance (Bin.Binary (l a1), Bin.Binary (r a1)) => Bin.Binary (S1 l r a1) -instance (Bin.Binary (l a2 a1), Bin.Binary (r a2 a1)) => Bin.Binary (S2 l r a2 a1) -instance (Bin.Binary (l a3 a2 a1), Bin.Binary (r a3 a2 a1)) => Bin.Binary (S3 l r a3 a2 a1) -instance (Bin.Binary (l a4 a3 a2 a1), Bin.Binary (r a4 a3 a2 a1)) => Bin.Binary (S4 l r a4 a3 a2 a1) -#endif - --------------------------------------------------------------------------------- -#ifdef VERSION_QuickCheck -instance (QC.Arbitrary (l a1), QC.Arbitrary (r a1)) => QC.Arbitrary (S1 l r a1) where - arbitrary = QC.oneof [ fmap S1L QC.arbitrary, fmap S1R QC.arbitrary ] - shrink (S1L l) = S1L <$> QC.shrink l - shrink (S1R r) = S1R <$> QC.shrink r -instance (QC.Arbitrary (l a2 a1), QC.Arbitrary (r a2 a1)) => QC.Arbitrary (S2 l r a2 a1) where - arbitrary = QC.oneof [ fmap S2L QC.arbitrary, fmap S2R QC.arbitrary ] - shrink (S2L l) = S2L <$> QC.shrink l - shrink (S2R r) = S2R <$> QC.shrink r -instance (QC.Arbitrary (l a3 a2 a1), QC.Arbitrary (r a3 a2 a1)) => QC.Arbitrary (S3 l r a3 a2 a1) where - arbitrary = QC.oneof [ fmap S3L QC.arbitrary, fmap S3R QC.arbitrary ] - shrink (S3L l) = S3L <$> QC.shrink l - shrink (S3R r) = S3R <$> QC.shrink r -instance (QC.Arbitrary (l a4 a3 a2 a1), QC.Arbitrary (r a4 a3 a2 a1)) => QC.Arbitrary (S4 l r a4 a3 a2 a1) where - arbitrary = QC.oneof [ fmap S4L QC.arbitrary, fmap S4R QC.arbitrary ] - shrink (S4L l) = S4L <$> QC.shrink l - shrink (S4R r) = S4R <$> QC.shrink r -#endif diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -9,6 +9,7 @@ module Main where import Control.DeepSeq (NFData(rnf)) +import qualified Codec.Serialise as Cborg import qualified Data.Aeson as Aeson import qualified Data.Binary as Bin import qualified Data.ByteString.Lazy as BSL @@ -27,7 +28,7 @@ import qualified Test.Tasty.QuickCheck as QC import Text.Read (readMaybe) -import Data.Singletons (SingKind, Sing, DemoteRep, withSomeSing) +import Data.Singletons (SingKind, Sing, Demote, withSomeSing) import Exinst @@ -50,6 +51,7 @@ , tt_id "Identity through Bytes's Serial" id_bytes , tt_id "Identity through Cereal's Serialize" id_cereal , tt_id "Identity through Binary's Binary" id_binary + , tt_id "Identity through serialise's Serialise" id_serialise , tt_id "Identity from Cereal's Serialize to Binary's Binary" id_cereal_to_binary , tt_id "Identity from Cereal's Serialize to Bytes's Serial" id_cereal_to_bytes , tt_id "Identity from Binary's Binary to Cereal's Serialize" id_binary_to_cereal @@ -64,7 +66,7 @@ -> (forall a. ( G.Generic a, Aeson.FromJSON a, Aeson.ToJSON a , Bytes.Serial a, Bin.Binary a, Cer.Serialize a - , Show a, Read a + , Cborg.Serialise a, Show a, Read a ) => a -> Maybe a ) -- ^ It's easier to put all the constraints here. -> Tasty.TestTree @@ -180,6 +182,12 @@ Right a' -> Just a' Left _ -> Nothing +id_serialise :: Cborg.Serialise a => a -> Maybe a +id_serialise = \a -> + case Cborg.deserialiseOrFail (Cborg.serialise a) of + Right a' -> Just a' + Left _ -> Nothing + id_cereal_to_binary :: (Bin.Binary a, Cer.Serialize a) => a -> Maybe a id_cereal_to_binary = \a -> case Bin.decodeOrFail (Cer.encodeLazy a) of @@ -219,42 +227,42 @@ -------------------------------------------------------------------------------- data family X1 :: Bool -> Type -data instance X1 'False = XF1 | XF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X1 'True = XT1 | XT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) +data instance X1 'False = XF1 | XF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X1 'True = XT1 | XT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) data family X2 :: Bool -> Bool -> Type -data instance X2 'False 'False = XFF1 | XFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X2 'False 'True = XFT1 | XFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X2 'True 'False = XTF1 | XTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X2 'True 'True = XTT1 | XTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) +data instance X2 'False 'False = XFF1 | XFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X2 'False 'True = XFT1 | XFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X2 'True 'False = XTF1 | XTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X2 'True 'True = XTT1 | XTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) data family X3 :: Bool -> Bool -> Bool -> Type -data instance X3 'False 'False 'False = XFFF1 | XFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X3 'False 'False 'True = XFFT1 | XFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X3 'False 'True 'False = XFTF1 | XFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X3 'False 'True 'True = XFTT1 | XFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X3 'True 'False 'False = XTFF1 | XTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X3 'True 'False 'True = XTFT1 | XTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X3 'True 'True 'False = XTTF1 | XTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X3 'True 'True 'True = XTTT1 | XTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) +data instance X3 'False 'False 'False = XFFF1 | XFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X3 'False 'False 'True = XFFT1 | XFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X3 'False 'True 'False = XFTF1 | XFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X3 'False 'True 'True = XFTT1 | XFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X3 'True 'False 'False = XTFF1 | XTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X3 'True 'False 'True = XTFT1 | XTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X3 'True 'True 'False = XTTF1 | XTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X3 'True 'True 'True = XTTT1 | XTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) data family X4 :: Bool -> Bool -> Bool -> Bool -> Type -data instance X4 'False 'False 'False 'False = XFFFF1 | XFFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'False 'False 'False 'True = XFFFT1 | XFFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'False 'False 'True 'False = XFFTF1 | XFFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'False 'False 'True 'True = XFFTT1 | XFFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'False 'True 'False 'False = XFTFF1 | XFTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'False 'True 'False 'True = XFTFT1 | XFTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'False 'True 'True 'False = XFTTF1 | XFTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'False 'True 'True 'True = XFTTT1 | XFTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'True 'False 'False 'False = XTFFF1 | XTFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'True 'False 'False 'True = XTFFT1 | XTFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'True 'False 'True 'False = XTFTF1 | XTFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'True 'False 'True 'True = XTFTT1 | XTFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'True 'True 'False 'False = XTTFF1 | XTTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'True 'True 'False 'True = XTTFT1 | XTTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'True 'True 'True 'False = XTTTF1 | XTTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) -data instance X4 'True 'True 'True 'True = XTTTT1 | XTTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, NFData, Hashable) +data instance X4 'False 'False 'False 'False = XFFFF1 | XFFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'False 'False 'False 'True = XFFFT1 | XFFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'False 'False 'True 'False = XFFTF1 | XFFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'False 'False 'True 'True = XFFTT1 | XFFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'False 'True 'False 'False = XFTFF1 | XFTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'False 'True 'False 'True = XFTFT1 | XFTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'False 'True 'True 'False = XFTTF1 | XFTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'False 'True 'True 'True = XFTTT1 | XFTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'True 'False 'False 'False = XTFFF1 | XTFFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'True 'False 'False 'True = XTFFT1 | XTFFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'True 'False 'True 'False = XTFTF1 | XTFTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'True 'False 'True 'True = XTFTT1 | XTFTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'True 'True 'False 'False = XTTFF1 | XTTFF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'True 'True 'False 'True = XTTFT1 | XTTFT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'True 'True 'True 'False = XTTTF1 | XTTTF2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) +data instance X4 'True 'True 'True 'True = XTTTT1 | XTTTT2 Int32 deriving (Eq, Show, Read, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, Bin.Binary, Cer.Serialize, Cborg.Serialise, NFData, Hashable) -------------------------------------------------------------------------------- -- Arbitrary instances