diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,18 @@ +# Version 0.4 + +* BREAKING: Decouple `binary` and `cereal` instances from `bytes`. This + introduces a slight backwards incompatible change if you were using some + `Serial` instances that depended on host endianness (such as `Int`). + +* Add `P1`, `P2`, `P3`, `P4`. + +* Add `S1`, `S2`, `S3`, `S4`. + +* Add `Read` instances for `Some{1,2,3,4}`. + +* Moved documentation from `README.md` into the top-level `Exinst` module. + + # Version 0.3.0.1 * Removed dependency on `generic-random`. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -2,531 +2,10 @@ [![Build Status](https://travis-ci.org/k0001/exinst.svg?branch=master)](https://travis-ci.org/k0001/exinst) -> See the [BSD3 LICENSE](https://github.com/k0001/exinst/blob/master/exinst/LICENSE.txt) -> file to learn about the legal terms and conditions for this library. - -Exinst is a library providing you with tools to automatically derive instances for -type-indexed types whose type-indexes have been existentialized. Currently it only -supports using [`singleton`](https://hackage.haskell.org/package/singletons) types as -type-indexes. - -> TODO: Support for non-singleton-types types with kind `*` using `Typeable` should -> be possible, but I haven't worked on that yet. It's on the roadmap. - -In short, what `exinst` currently gives you is: For any type ``t :: k -> *``, -if `k` is a singleton type and `c (t k) :: Constraint` is satisfied, then you can -existentialize away the `k` parameter with `Some1 t`, 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 `()`. - -## Motivation - -As a motivation, let's consider the following example: - -```haskell -{-# 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. - -```haskell ---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`. - -```haskell -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: - -```haskell -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. - - -## 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 TH provided by `Data.Singletons.TH`: - -```haskell -import 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: - -```haskell -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) -> import Exinst.Instances.Base () -> :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. - -> TODO: Implement said `Read` instance. - -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: - -```haskell -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. - -```haskell --- The Exinst.Dict1 class -class Dict1 (c :: * -> Constraint) (f1 :: k1 -> *) 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. Even *boilerplatey* if you -will; they could even be generated using TH - -> TODO: Write the TH for deriving the `Dict{1,2,3,4}` implementation. - -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 -> *` 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: - -```haskell -instance (c (f1 'Small), c (f1 'Big)) => Dict1 c f1 where - dict1 = \x -> case x of - SSmall -> Dict - SBig -> Dict -``` - -That instance says that for any choice of `c` and `f1 :: Size -> *`, 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 with some cabal flags). - -* `Eq`, `Ord`, `Show` from the `base` package. - -* `FromJSON` and `ToJSON` from the `aeson` package. - -* `Serial` from the `bytes` package. - -* `Hashable` from the `hashable` package. - -* `NFData` from the `deepseq` package. - -* `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 :: k -> *)`, then make sure an instance -for `Z` is available for the `DemoteRep ('KProxy :: KProxy k)`, that a `Dict1 Z -(f :: k -> *)` or more general instance exists, and that the `Y` instance for -`Some1 (f :: k -> *)` exists too. - -Here is the full code needed to have, say, the `Eq`, `Show`, `ToJSON` and -`FromJSON` instances available for `Some1 Receptacle`: - -```haskell -{-# 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.Aeson as Ae -import Data.Constraint (Dict(Dict)) -import qualified Data.Singletons.TH -import Exinst (Dict1(dict1)) - ------ - -data Size = Big | Small - deriving (Eq, Show) - -Data.Singletons.TH.genSingletons [''Size] -Data.Singletons.TH.singDecideInstances [''Size] - -instance Ae.ToJSON Size where - toJSON = \x -> case x of - Small -> Ae.toJSON ("Small" :: String) - Big -> Ae.toJSON ("Big" :: String) - -instance Ae.FromJSON Size where - parseJSON = Ae.withText "Size" $ \t -> case t of - "Big" -> return Big - "Small" -> return Small - _ -> fail "Unknown" - - -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) - -instance Ae.ToJSON (Receptacle a) where - toJSON = \x -> case x of - Vase -> Ae.toJSON ("Vase" :: String) - Glass -> Ae.toJSON ("Glass" :: String) - Barrel -> Ae.toJSON ("Barrel" :: String) - -instance Ae.FromJSON (Receptacle 'Small) where - parseJSON = Ae.withText "Receptacle 'Small" $ \t -> case t of - "Vase" -> return Vase - "Glass" -> return Glass - _ -> fail "Unknown" - -instance Ae.FromJSON (Receptacle 'Big) where - parseJSON = Ae.withText "Receptacle 'Big" $ \t -> case t of - "Barrel" -> return Barrel - _ -> fail "Unknown" -``` - -Now, provided that we import `Exinst.Instances.Base` and -`Exinst.Instances.Aeson`, `Some1 Receptacle` will have `Eq`, `Show`, `FromJSON` -and `FromJSON` instances: - -``` -> import Exinst.Instances.Base () -> import Exinst.Instances.Aeson () - -> -- 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"] - -> -- Trying the `ToJSON` and `FromJSON` instances. -> Ae.encode (some1 Vase) -"[\"Small\",\"Vase\"]" -- Just like in Show, the ToJSON adds some information - -- about the Size type-index. That's why we require - -- Size to provide a ToJSON instance too. -> Ae.decode (Ae.encode (some1 Vase)) == Just (some1 Vase) -True -> Ae.decode (Ae.encode (some1 Vase)) == Just (some1 Glass) -False -``` - - -## About `Some2`, `Some3` and `Some4`. - -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: - -```haskell -instance (c (f1 'T1a), c (f1 'T1b)) => Dict1 c (f1 :: T1 -> *) where - dict1 = \x -> case x of { ST1a -> Dict; ST1b -> Dict } -instance (Dict1 c (f2 'T2a), Dict1 c (f2 'T2b)) => Dict2 c (f2 :: T2 -> k1 -> *) 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 -> *) 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 -> *) where - dict4 = \x -> case x of { ST4a -> dict3; ST4b -> dict3 } -``` - -That is, assuming the following `T1`, `T2`, `T3` and `T4`: - -```haskell -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`. - -> TODO: See if instead of having `Some1`, `Some2`, `Some3`, `Some4`, and their -> respective `Dict1`, `Dict2`, `Dict3` and `Dict4`, etc., we can have a single -> `SomeN` and a single `DictN` working out the number of parameters using -> type-level natural numbers. - -## Converting `Some1 (f :: k -> *)` to `f (a :: k)`. - -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 TH 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). - - -# Library implementors: Writing instances for `Some1` and friends. - -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. - -When we imported `Exinst.Instances.Base` before, we brought to scope, among -other things, the `Show` instance for `Some1`, which is defined as this: - -```haskell --- Internal wrapper so that we don't have to write the string manipulation parts --- in the 'Show' instance by hand. -data Some1'Show r1 x = Some1 r1 x deriving (Show) - -instance forall (f1 :: k1 -> *) - . ( SingKind ('KProxy :: KProxy k1) - , Show (DemoteRep ('KProxy :: KProxy k1)) - , Dict1 Show f1 - ) => Show (Some1 f1) - where - showsPrec n = \some1 -> withSome1Sing some1 $ \sa1 (x :: f1 a1) -> - case dict1 sa1 :: Dict (Show (f1 a1)) of - Dict -> showsPrec n (Some1 (fromSing sa1) x) -``` - -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`. +See the [BSD3 LICENSE](https://github.com/k0001/exinst/blob/master/exinst/LICENSE.txt) +file to learn about the legal terms and conditions for this library. +Find documentation for this library in the top-level +[`Exinst`](https://github.com/k0001/exinst/blob/master/exinst/src/lib/Exinst.hs) +module. diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,2 +1,4 @@ +#! /usr/bin/env nix-shell +#! nix-shell ./shell.nix -i runghc import Distribution.Simple main = defaultMain diff --git a/exinst.cabal b/exinst.cabal --- a/exinst.cabal +++ b/exinst.cabal @@ -1,5 +1,5 @@ name: exinst -version: 0.3.0.1 +version: 0.4 author: Renzo Carbonara maintainer: renzoλcarbonara.com.ar copyright: Renzo Carbonara 2015-2017 @@ -9,7 +9,7 @@ category: Data build-type: Simple cabal-version: >=1.18 -synopsis: Recover instances for your existential types. +synopsis: Recover type indexes and instances for your existentialized types. homepage: https://github.com/k0001/exinst bug-reports: https://github.com/k0001/exinst/issues @@ -21,6 +21,8 @@ Exinst other-modules: Exinst.Internal + Exinst.Internal.Product + Exinst.Internal.Sum Exinst.Instances.Base build-depends: base >=4.9 && <5.0 @@ -33,9 +35,15 @@ if flag(aeson) build-depends: aeson other-modules: Exinst.Instances.Aeson + if flag(binary) || flag(bytes) + build-depends: binary + other-modules: Exinst.Instances.Binary if flag(bytes) - build-depends: bytes >=0.15, binary, cereal + build-depends: bytes >=0.15 other-modules: Exinst.Instances.Bytes + if flag(cereal) || flag(bytes) + build-depends: cereal + other-modules: Exinst.Instances.Cereal if flag(deepseq) build-depends: deepseq other-modules: Exinst.Instances.DeepSeq @@ -50,7 +58,7 @@ test-suite tests default-language: Haskell2010 type: exitcode-stdio-1.0 - hs-source-dirs: tests + hs-source-dirs: tests src/lib main-is: Main.hs build-depends: aeson @@ -61,7 +69,6 @@ , cereal , constraints , deepseq - , exinst , hashable , profunctors , QuickCheck @@ -76,7 +83,15 @@ default: True manual: True flag bytes - description: Provide instances for @bytes@, @binary@ and @cereal@. + description: Provide instances for @bytes@ (implies @ceral@ and @binary@). + default: True + manual: True +flag binary + description: Provide instances for @binary@. + default: True + manual: True +flag cereal + description: Provide instances for @cereal@. default: True manual: True flag deepseq diff --git a/src/lib/Exinst.hs b/src/lib/Exinst.hs --- a/src/lib/Exinst.hs +++ b/src/lib/Exinst.hs @@ -1,8 +1,49 @@ {-# LANGUAGE CPP #-} --- | See the README file for documentation: https://hackage.haskell.org/package/exinst#readme +{- | + +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 - ( -- * 1 type index + ( -- * Tutorial + -- $motivation + + -- *** Usage + -- $usage + + -- *** Recovering + -- $recovering + + -- *** Many indexes + -- $manyIndexes + + -- *** Writing instances + -- $writingInstances + + -- *** Products and sums + -- $prodsums + + -- * 1 type index Some1(Some1) , some1 , fromSome1 @@ -45,24 +86,51 @@ -- * 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 @@ -74,3 +142,536 @@ #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 --- a/src/lib/Exinst/Instances/Aeson.hs +++ b/src/lib/Exinst/Instances/Aeson.hs @@ -22,46 +22,46 @@ -------------------------------------------------------------------------------- -instance forall (f1 :: k1 -> *) +instance forall (f :: k1 -> *) . ( SingKind k1 , Ae.ToJSON (DemoteRep k1) - , Dict1 Ae.ToJSON f1 - ) => Ae.ToJSON (Some1 f1) + , Dict1 Ae.ToJSON f + ) => Ae.ToJSON (Some1 f) where {-# INLINABLE toJSON #-} - toJSON = \some1x -> withSome1Sing some1x $ \sa1 (x :: f1 a1) -> - case dict1 sa1 :: Dict (Ae.ToJSON (f1 a1)) of + 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 (f2 :: k2 -> k1 -> *) +instance forall (f :: k2 -> k1 -> *) . ( SingKind k2 , SingKind k1 , Ae.ToJSON (DemoteRep k2) , Ae.ToJSON (DemoteRep k1) - , Dict2 Ae.ToJSON f2 - ) => Ae.ToJSON (Some2 f2) + , Dict2 Ae.ToJSON f + ) => Ae.ToJSON (Some2 f) where {-# INLINABLE toJSON #-} - toJSON = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f2 a2 a1) -> - case dict2 sa2 sa1 :: Dict (Ae.ToJSON (f2 a2 a1)) of + 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 (f3 :: k3 -> k2 -> k1 -> *) +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 f3 - ) => Ae.ToJSON (Some3 f3) + , Dict3 Ae.ToJSON f + ) => Ae.ToJSON (Some3 f) where {-# INLINABLE toJSON #-} - toJSON = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f3 a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f3 a3 a2 a1)) of + 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 (f4 :: k4 -> k3 -> k2 -> k1 -> *) +instance forall (f :: k4 -> k3 -> k2 -> k1 -> *) . ( SingKind k4 , SingKind k3 , SingKind k2 @@ -70,71 +70,71 @@ , Ae.ToJSON (DemoteRep k3) , Ae.ToJSON (DemoteRep k2) , Ae.ToJSON (DemoteRep k1) - , Dict4 Ae.ToJSON f4 - ) => Ae.ToJSON (Some4 f4) + , Dict4 Ae.ToJSON f + ) => Ae.ToJSON (Some4 f) where {-# INLINABLE toJSON #-} - toJSON = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f4 a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.ToJSON (f4 a4 a3 a2 a1)) of + 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 (f1 :: k1 -> *) +instance forall (f :: k1 -> *) . ( SingKind k1 , Ae.FromJSON (DemoteRep k1) - , Dict1 Ae.FromJSON f1 - ) => Ae.FromJSON (Some1 f1) + , 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)) -> withSingI sa1 $ - case dict1 sa1 :: Dict (Ae.FromJSON (f1 a1)) of + withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> + case dict1 sa1 :: Dict (Ae.FromJSON (f a1)) of Dict -> do - x :: f1 a1 <- Ae.parseJSON v' - return (some1 x) + x :: f a1 <- Ae.parseJSON v' + pure (Some1 sa1 x) -instance forall (f2 :: k2 -> k1 -> *) +instance forall (f :: k2 -> k1 -> *) . ( SingKind k2 , SingKind k1 , Ae.FromJSON (DemoteRep k2) , Ae.FromJSON (DemoteRep k1) - , Dict2 Ae.FromJSON f2 - ) => Ae.FromJSON (Some2 f2) + , 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)) -> withSingI sa2 $ - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $ - case dict2 sa2 sa1 :: Dict (Ae.FromJSON (f2 a2 a1)) of + 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 :: f2 a2 a1 <- Ae.parseJSON v' - return (some2 x) + x :: f a2 a1 <- Ae.parseJSON v' + pure (Some2 sa2 sa1 x) -instance forall (f3 :: k3 -> k2 -> k1 -> *) +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 f3 - ) => Ae.FromJSON (Some3 f3) + , 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)) -> withSingI sa3 $ - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $ - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $ - case dict3 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f3 a3 a2 a1)) of + 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 :: f3 a3 a2 a1 <- Ae.parseJSON v' - return (some3 x) + x :: f a3 a2 a1 <- Ae.parseJSON v' + pure (Some3 sa3 sa2 sa1 x) -instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) +instance forall (f :: k4 -> k3 -> k2 -> k1 -> *) . ( SingKind k4 , SingKind k3 , SingKind k2 @@ -143,17 +143,17 @@ , Ae.FromJSON (DemoteRep k3) , Ae.FromJSON (DemoteRep k2) , Ae.FromJSON (DemoteRep k1) - , Dict4 Ae.FromJSON f4 - ) => Ae.FromJSON (Some4 f4) + , 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)) -> withSingI sa4 $ - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> withSingI sa3 $ - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $ - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $ - case dict4 sa4 sa3 sa2 sa1 :: Dict (Ae.FromJSON (f4 a4 a3 a2 a1)) of + 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 :: f4 a4 a3 a2 a1 <- Ae.parseJSON v' - return (some4 x) + 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 --- a/src/lib/Exinst/Instances/Base.hs +++ b/src/lib/Exinst/Instances/Base.hs @@ -30,62 +30,61 @@ 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' +-- 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) --------------------------------------------------------------------------------- --- Show - -instance forall (f1 :: k1 -> Type) +instance forall (f :: k1 -> Type) . ( SingKind k1 , Show (DemoteRep k1) - , Dict1 Show f1 - ) => Show (Exinst.Some1 f1) + , Dict1 Show f + ) => Show (Exinst.Some1 f) where {-# INLINABLE showsPrec #-} - showsPrec n = \some1x -> withSome1Sing some1x $ \sa1 (x :: f1 a1) -> - case dict1 sa1 :: Dict (Show (f1 a1)) of + 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 (f2 :: k2 -> k1 -> Type) +instance forall (f :: k2 -> k1 -> Type) . ( SingKind k2 , SingKind k1 , Show (DemoteRep k2) , Show (DemoteRep k1) - , Dict2 Show f2 - ) => Show (Exinst.Some2 f2) + , Dict2 Show f + ) => Show (Exinst.Some2 f) where {-# INLINABLE showsPrec #-} - showsPrec n = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f2 a2 a1) -> - case dict2 sa2 sa1 :: Dict (Show (f2 a2 a1)) of + 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 (f3 :: k3 -> k2 -> k1 -> Type) +instance forall (f :: k3 -> k2 -> k1 -> Type) . ( SingKind k3 , SingKind k2 , SingKind k1 , Show (DemoteRep k3) , Show (DemoteRep k2) , Show (DemoteRep k1) - , Dict3 Show f3 - ) => Show (Exinst.Some3 f3) + , Dict3 Show f + ) => Show (Exinst.Some3 f) where {-# INLINABLE showsPrec #-} - showsPrec n = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f3 a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Show (f3 a3 a2 a1)) of + 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 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) +instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) . ( SingKind k4 , SingKind k3 , SingKind k2 @@ -94,134 +93,222 @@ , Show (DemoteRep k3) , Show (DemoteRep k2) , Show (DemoteRep k1) - , Dict4 Show f4 - ) => Show (Exinst.Some4 f4) + , Dict4 Show f + ) => Show (Exinst.Some4 f) where {-# INLINABLE showsPrec #-} - showsPrec n = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f4 a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Show (f4 a4 a3 a2 a1)) of + 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 (f1 :: k1 -> Type) - . ( SDecide k1 - , Dict1 Eq f1 - ) => Eq (Exinst.Some1 f1) +instance forall (f :: k1 -> Type). + ( SDecide k1 + , Dict1 Eq f + ) => Eq (Exinst.Some1 f) where - {-# INLINABLE (==) #-} - (==) = \som1x som1y -> - withSome1Sing som1x $ \sa1x (x :: f1 a1x) -> - withSome1Sing som1y $ \sa1y (y :: f1 a1y) -> - maybe False id $ do - Refl <- testEquality sa1x sa1y - case dict1 sa1x :: Dict (Eq (f1 a1x)) of - Dict -> Just (x == y) + {-# 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 (f2 :: k2 -> k1 -> Type) +instance forall (f :: k2 -> k1 -> Type) . ( SDecide k2 , SDecide k1 - , Dict2 Eq f2 - ) => Eq (Exinst.Some2 f2) + , Dict2 Eq f + ) => Eq (Exinst.Some2 f) where {-# INLINABLE (==) #-} (==) = \som2x som2y -> - withSome2Sing som2x $ \sa2x sa1x (x :: f2 a2x a1x) -> - withSome2Sing som2y $ \sa2y sa1y (y :: f2 a2y a1y) -> + 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 (f2 a2x a1x)) of + case dict2 sa2x sa1x :: Dict (Eq (f a2x a1x)) of Dict -> Just (x == y) -instance forall (f3 :: k3 -> k2 -> k1 -> Type) +instance forall (f :: k3 -> k2 -> k1 -> Type) . ( SDecide k3 , SDecide k2 , SDecide k1 - , Dict3 Eq f3 - ) => Eq (Exinst.Some3 f3) + , Dict3 Eq f + ) => Eq (Exinst.Some3 f) where {-# INLINABLE (==) #-} (==) = \som3x som3y -> - withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f3 a3x a2x a1x) -> - withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f3 a3y a2y a1y) -> + 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 (f3 a3x a2x a1x)) of + case dict3 sa3x sa2x sa1x :: Dict (Eq (f a3x a2x a1x)) of Dict -> Just (x == y) -instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) +instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) . ( SDecide k4 , SDecide k3 , SDecide k2 , SDecide k1 - , Dict4 Eq f4 - ) => Eq (Exinst.Some4 f4) + , Dict4 Eq f + ) => Eq (Exinst.Some4 f) where {-# INLINABLE (==) #-} (==) = \som4x som4y -> - withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f4 a4x a3x a2x a1x) -> - withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f4 a4y a3y a2y a1y) -> + 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 (f4 a4x a3x a2x a1x)) of + case dict4 sa4x sa3x sa2x sa1x :: Dict (Eq (f a4x a3x a2x a1x)) of Dict -> Just (x == y) -------------------------------------------------------------------------------- -- Ord -instance forall (f1 :: k1 -> Type) +instance forall (f :: k1 -> Type) . ( SingKind k1 , SDecide k1 , Ord (DemoteRep k1) - , Dict1 Ord f1 - , Eq (Exinst.Some1 f1) - ) => Ord (Exinst.Some1 f1) + , Dict1 Ord f + , Eq (Exinst.Some1 f) + ) => Ord (Exinst.Some1 f) where {-# INLINABLE compare #-} compare = \som1x som1y -> - withSome1Sing som1x $ \sa1x (x :: f1 a1x) -> - withSome1Sing som1y $ \sa1y (y :: f1 a1y) -> + 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 (f1 a1x)) of + case dict1 sa1x :: Dict (Ord (f a1x)) of Dict -> Just (compare x y) -instance forall (f2 :: k2 -> k1 -> Type) +instance forall (f :: k2 -> k1 -> Type) . ( SingKind k2 , SingKind k1 , SDecide k2 , SDecide k1 , Ord (DemoteRep k2) , Ord (DemoteRep k1) - , Dict2 Ord f2 - , Eq (Exinst.Some2 f2) - ) => Ord (Exinst.Some2 f2) + , Dict2 Ord f + , Eq (Exinst.Some2 f) + ) => Ord (Exinst.Some2 f) where {-# INLINABLE compare #-} compare = \som2x som2y -> - withSome2Sing som2x $ \sa2x sa1x (x :: f2 a2x a1x) -> - withSome2Sing som2y $ \sa2y sa1y (y :: f2 a2y a1y) -> + 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 (f2 a2x a1x)) of + case dict2 sa2x sa1x :: Dict (Ord (f a2x a1x)) of Dict -> Just (compare x y) -instance forall (f3 :: k3 -> k2 -> k1 -> Type) +instance forall (f :: k3 -> k2 -> k1 -> Type) . ( SingKind k3 , SingKind k2 , SingKind k1 @@ -231,14 +318,14 @@ , Ord (DemoteRep k3) , Ord (DemoteRep k2) , Ord (DemoteRep k1) - , Dict3 Ord f3 - , Eq (Exinst.Some3 f3) - ) => Ord (Exinst.Some3 f3) + , Dict3 Ord f + , Eq (Exinst.Some3 f) + ) => Ord (Exinst.Some3 f) where {-# INLINABLE compare #-} compare = \som3x som3y -> - withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f3 a3x a2x a1x) -> - withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f3 a3y a2y a1y) -> + 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) @@ -246,10 +333,10 @@ Refl <- testEquality sa3x sa3y Refl <- testEquality sa2x sa2y Refl <- testEquality sa1x sa1y - case dict3 sa3x sa2x sa1x :: Dict (Ord (f3 a3x a2x a1x)) of + case dict3 sa3x sa2x sa1x :: Dict (Ord (f a3x a2x a1x)) of Dict -> Just (compare x y) -instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) +instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type) . ( SingKind k4 , SingKind k3 , SingKind k2 @@ -262,14 +349,14 @@ , Ord (DemoteRep k3) , Ord (DemoteRep k2) , Ord (DemoteRep k1) - , Dict4 Ord f4 - , Eq (Exinst.Some4 f4) - ) => Ord (Exinst.Some4 f4) + , Dict4 Ord f + , Eq (Exinst.Some4 f) + ) => Ord (Exinst.Some4 f) where {-# INLINABLE compare #-} compare = \som4x som4y -> - withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f4 a4x a3x a2x a1x) -> - withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f4 a4y a3y a2y a1y) -> + 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) @@ -278,7 +365,7 @@ Refl <- testEquality sa3x sa3y Refl <- testEquality sa2x sa2y Refl <- testEquality sa1x sa1y - case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f4 a4x a3x a2x a1x)) of + case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f a4x a3x a2x a1x)) of Dict -> Just (compare x y) -------------------------------------------------------------------------------- diff --git a/src/lib/Exinst/Instances/Binary.hs b/src/lib/Exinst/Instances/Binary.hs new file mode 100644 --- /dev/null +++ b/src/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 '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 --- a/src/lib/Exinst/Instances/Bytes.hs +++ b/src/lib/Exinst/Instances/Bytes.hs @@ -14,8 +14,6 @@ module Exinst.Instances.Bytes () where import qualified Data.Bytes.Serial as By -import qualified Data.Binary as Bin -import qualified Data.Serialize as Cer import Data.Constraint import Data.Singletons import Prelude @@ -24,152 +22,117 @@ -------------------------------------------------------------------------------- -instance forall (f1 :: k1 -> *) - . ( SingKind k1 - , By.Serial (DemoteRep k1) - , Dict1 By.Serial f1 - ) => By.Serial (Some1 f1) - where - {-# INLINABLE serialize #-} - serialize = \some1x -> withSome1Sing some1x $ \sa1 (x :: f1 a1) -> - case dict1 sa1 :: Dict (By.Serial (f1 a1)) of - Dict -> do By.serialize (fromSing sa1) - By.serialize x - {-# INLINABLE deserialize #-} - deserialize = do - rsa1 <- By.deserialize - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $ - case dict1 sa1 :: Dict (By.Serial (f1 a1)) of - Dict -> do x :: f1 a1 <- By.deserialize - return (some1 x) - -instance forall (f2 :: k2 -> k1 -> *) - . ( SingKind k2 - , SingKind k1 - , By.Serial (DemoteRep k2) - , By.Serial (DemoteRep k1) - , Dict2 By.Serial f2 - ) => By.Serial (Some2 f2) - where - {-# INLINABLE serialize #-} - serialize = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f2 a2 a1) -> - case dict2 sa2 sa1 :: Dict (By.Serial (f2 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)) -> withSingI sa2 $ - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $ - case dict2 sa2 sa1 :: Dict (By.Serial (f2 a2 a1)) of - Dict -> do x :: f2 a2 a1 <- By.deserialize - return (some2 x) - -instance forall (f3 :: k3 -> k2 -> k1 -> *) - . ( SingKind k3 - , SingKind k2 - , SingKind k1 - , By.Serial (DemoteRep k3) - , By.Serial (DemoteRep k2) - , By.Serial (DemoteRep k1) - , Dict3 By.Serial f3 - ) => By.Serial (Some3 f3) - where - {-# INLINABLE serialize #-} - serialize = \some3x -> withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f3 a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f3 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)) -> withSingI sa3 $ - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $ - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $ - case dict3 sa3 sa2 sa1 :: Dict (By.Serial (f3 a3 a2 a1)) of - Dict -> do x :: f3 a3 a2 a1 <- By.deserialize - return (some3 x) - -instance forall (f4 :: 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 f4 - ) => By.Serial (Some4 f4) - where - {-# INLINABLE serialize #-} - serialize = \some4x -> withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f4 a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f4 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)) -> withSingI sa4 $ - withSomeSing rsa3 $ \(sa3 :: Sing (a3 :: k3)) -> withSingI sa3 $ - withSomeSing rsa2 $ \(sa2 :: Sing (a2 :: k2)) -> withSingI sa2 $ - withSomeSing rsa1 $ \(sa1 :: Sing (a1 :: k1)) -> withSingI sa1 $ - case dict4 sa4 sa3 sa2 sa1 :: Dict (By.Serial (f4 a4 a3 a2 a1)) of - Dict -> do x :: f4 a4 a3 a2 a1 <- By.deserialize - return (some4 x) - --------------------------------------------------------------------------------- --- Binary - -instance By.Serial (Some1 f) => Bin.Binary (Some1 f) where - {-# INLINE put #-} - put = By.serialize - {-# INLINE get #-} - get = By.deserialize - -instance By.Serial (Some2 f) => Bin.Binary (Some2 f) where - {-# INLINE put #-} - put = By.serialize - {-# INLINE get #-} - get = By.deserialize - -instance By.Serial (Some3 f) => Bin.Binary (Some3 f) where - {-# INLINE put #-} - put = By.serialize - {-# INLINE get #-} - get = By.deserialize - -instance By.Serial (Some4 f) => Bin.Binary (Some4 f) where - {-# INLINE put #-} - put = By.serialize - {-# INLINE get #-} - get = By.deserialize - --------------------------------------------------------------------------------- --- Cereal - -instance By.Serial (Some1 f) => Cer.Serialize (Some1 f) where - {-# INLINE put #-} - put = By.serialize - {-# INLINE get #-} - get = By.deserialize - -instance By.Serial (Some2 f) => Cer.Serialize (Some2 f) where - {-# INLINE put #-} - put = By.serialize - {-# INLINE get #-} - get = By.deserialize +-- | 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) -instance By.Serial (Some3 f) => Cer.Serialize (Some3 f) where - {-# INLINE put #-} - put = By.serialize - {-# INLINE get #-} - get = By.deserialize +-- | 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) -instance By.Serial (Some4 f) => Cer.Serialize (Some4 f) where - {-# INLINE put #-} - put = By.serialize - {-# INLINE get #-} - get = By.deserialize +-- | 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 new file mode 100644 --- /dev/null +++ b/src/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 '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 --- a/src/lib/Exinst/Instances/DeepSeq.hs +++ b/src/lib/Exinst/Instances/DeepSeq.hs @@ -22,39 +22,39 @@ -------------------------------------------------------------------------------- -instance forall (f1 :: k1 -> *). - ( Dict1 NFData f1 - ) => NFData (Some1 f1) where +instance forall (f :: k1 -> *). + ( Dict1 NFData f + ) => NFData (Some1 f) where {-# INLINABLE rnf #-} rnf = \(!some1x) -> - withSome1Sing some1x $ \ !sa1 !(x :: f1 a1) -> - case dict1 sa1 :: Dict (NFData (f1 a1)) of + withSome1Sing some1x $ \ !sa1 !(x :: f a1) -> + case dict1 sa1 :: Dict (NFData (f a1)) of Dict -> rnf x `seq` () -instance forall (f2 :: k2 -> k1 -> *). - ( Dict2 NFData f2 - ) => NFData (Some2 f2) where +instance forall (f :: k2 -> k1 -> *). + ( Dict2 NFData f + ) => NFData (Some2 f) where {-# INLINABLE rnf #-} rnf = \(!some2x) -> - withSome2Sing some2x $ \ !sa2 !sa1 !(x :: f2 a2 a1) -> - case dict2 sa2 sa1 :: Dict (NFData (f2 a2 a1)) of + withSome2Sing some2x $ \ !sa2 !sa1 !(x :: f a2 a1) -> + case dict2 sa2 sa1 :: Dict (NFData (f a2 a1)) of Dict -> rnf x `seq` () -instance forall (f3 :: k3 -> k2 -> k1 -> *). - ( Dict3 NFData f3 - ) => NFData (Some3 f3) where +instance forall (f :: k3 -> k2 -> k1 -> *). + ( Dict3 NFData f + ) => NFData (Some3 f) where {-# INLINABLE rnf #-} rnf = \(!some3x) -> - withSome3Sing some3x $ \ !sa3 !sa2 !sa1 !(x :: f3 a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (NFData (f3 a3 a2 a1)) of + 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 (f4 :: k4 -> k3 -> k2 -> k1 -> *). - ( Dict4 NFData f4 - ) => NFData (Some4 f4) where +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 :: f4 a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (NFData (f4 a4 a3 a2 a1)) of + 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 --- a/src/lib/Exinst/Instances/Hashable.hs +++ b/src/lib/Exinst/Instances/Hashable.hs @@ -28,55 +28,55 @@ -------------------------------------------------------------------------------- -instance forall (f1 :: k1 -> *) +instance forall (f :: k1 -> *) . ( SingKind k1 , Hashable (DemoteRep k1) - , Dict1 Hashable f1 - ) => Hashable (Some1 f1) + , Dict1 Hashable f + ) => Hashable (Some1 f) where {-# INLINABLE hashWithSalt #-} - hashWithSalt salt some1x = withSome1Sing some1x $ \sa1 (x :: f1 a1) -> - case dict1 sa1 :: Dict (Hashable (f1 a1)) of + 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 (f2 :: k2 -> k1 -> *) +instance forall (f :: k2 -> k1 -> *) . ( SingKind k2 , SingKind k1 , Hashable (DemoteRep k2) , Hashable (DemoteRep k1) - , Dict2 Hashable f2 - ) => Hashable (Some2 f2) + , Dict2 Hashable f + ) => Hashable (Some2 f) where {-# INLINABLE hashWithSalt #-} - hashWithSalt salt some2x = withSome2Sing some2x $ \sa2 sa1 (x :: f2 a2 a1) -> - case dict2 sa2 sa1 :: Dict (Hashable (f2 a2 a1)) of + 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 (f3 :: k3 -> k2 -> k1 -> *) +instance forall (f :: k3 -> k2 -> k1 -> *) . ( SingKind k3 , SingKind k2 , SingKind k1 , Hashable (DemoteRep k3) , Hashable (DemoteRep k2) , Hashable (DemoteRep k1) - , Dict3 Hashable f3 - ) => Hashable (Some3 f3) + , Dict3 Hashable f + ) => Hashable (Some3 f) where {-# INLINABLE hashWithSalt #-} - hashWithSalt salt some3x = withSome3Sing some3x $ \sa3 sa2 sa1 (x :: f3 a3 a2 a1) -> - case dict3 sa3 sa2 sa1 :: Dict (Hashable (f3 a3 a2 a1)) of + 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 (f4 :: k4 -> k3 -> k2 -> k1 -> *) +instance forall (f :: k4 -> k3 -> k2 -> k1 -> *) . ( SingKind k4 , SingKind k3 , SingKind k2 @@ -85,12 +85,12 @@ , Hashable (DemoteRep k3) , Hashable (DemoteRep k2) , Hashable (DemoteRep k1) - , Dict4 Hashable f4 - ) => Hashable (Some4 f4) + , Dict4 Hashable f + ) => Hashable (Some4 f) where {-# INLINABLE hashWithSalt #-} - hashWithSalt salt some4x = withSome4Sing some4x $ \sa4 sa3 sa2 sa1 (x :: f4 a4 a3 a2 a1) -> - case dict4 sa4 sa3 sa2 sa1 :: Dict (Hashable (f4 a4 a3 a2 a1)) of + 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 diff --git a/src/lib/Exinst/Internal/Product.hs b/src/lib/Exinst/Internal/Product.hs new file mode 100644 --- /dev/null +++ b/src/lib/Exinst/Internal/Product.hs @@ -0,0 +1,139 @@ +{-# 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 new file mode 100644 --- /dev/null +++ b/src/lib/Exinst/Internal/Sum.hs @@ -0,0 +1,143 @@ +{-# 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 @@ -15,15 +15,17 @@ import qualified Data.Bytes.Get as Bytes import qualified Data.Bytes.Put as Bytes import qualified Data.Bytes.Serial as Bytes -import qualified Data.Serialize as Cer import Data.Hashable (Hashable(hash)) +import Data.Int (Int32) import Data.Kind (Type) import Data.Proxy (Proxy) +import qualified Data.Serialize as Cer import qualified GHC.Generics as G import qualified Test.Tasty as Tasty import qualified Test.Tasty.Runners as Tasty import Test.Tasty.QuickCheck ((===)) import qualified Test.Tasty.QuickCheck as QC +import Text.Read (readMaybe) import Data.Singletons (SingKind, Sing, DemoteRep, withSomeSing) @@ -42,11 +44,18 @@ tt :: Tasty.TestTree tt = Tasty.testGroup "main" - [ tt_id "Identity through GHC's Generic" id_generic - , tt_id "Identity through Aeson's FromJSON/ToJSON" id_aeson + [ tt_id "Identity through Show/Read" id_show_read + , tt_id "Identity through GHC's Generic" id_generic + , tt_id "Identity through Aeson's ToJSON/FromJSON" id_aeson , 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 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 + , tt_id "Identity from Binary's Binary to Bytes's Serial" id_binary_to_bytes + , tt_id "Identity from Bytes's Serial to Binary's Binary" id_bytes_to_binary + , tt_id "Identity from Bytes's Serial to Cereal's Serialize" id_bytes_to_cereal , tt_nfdata ] @@ -55,46 +64,98 @@ -> (forall a. ( G.Generic a, Aeson.FromJSON a, Aeson.ToJSON a , Bytes.Serial a, Bin.Binary a, Cer.Serialize a + , Show a, Read a ) => a -> Maybe a ) -- ^ It's easier to put all the constraints here. -> Tasty.TestTree tt_id = \title id' -> Tasty.testGroup title - [ QC.testProperty "Some1" $ - QC.forAll QC.arbitrary $ \(x :: Some1 Foo1) -> Just x === id' x - , QC.testProperty "Some2" $ - QC.forAll QC.arbitrary $ \(x :: Some2 Foo2) -> Just x === id' x - , QC.testProperty "Some3" $ - QC.forAll QC.arbitrary $ \(x :: Some3 Foo3) -> Just x === id' x - , QC.testProperty "Some4" $ - QC.forAll QC.arbitrary $ \(x :: Some4 Foo4) -> Just x === id' x + [ QC.testProperty "Some1 X1" $ + QC.forAll QC.arbitrary $ \(x :: Some1 X1) -> Just x === id' x + , QC.testProperty "Some2 X2" $ + QC.forAll QC.arbitrary $ \(x :: Some2 X2) -> Just x === id' x + , QC.testProperty "Some3 X3" $ + QC.forAll QC.arbitrary $ \(x :: Some3 X3) -> Just x === id' x + , QC.testProperty "Some4 X4" $ + QC.forAll QC.arbitrary $ \(x :: Some4 X4) -> Just x === id' x + , QC.testProperty "Some1 (P1 X1 X1)" $ + QC.forAll QC.arbitrary $ \(x :: Some1 (P1 X1 X1)) -> Just x === id' x + , QC.testProperty "Some2 (P2 X2 X2)" $ + QC.forAll QC.arbitrary $ \(x :: Some2 (P2 X2 X2)) -> Just x === id' x + , QC.testProperty "Some3 (P3 X3 X3)" $ + QC.forAll QC.arbitrary $ \(x :: Some3 (P3 X3 X3)) -> Just x === id' x + , QC.testProperty "Some4 (P4 X4 X4)" $ + QC.forAll QC.arbitrary $ \(x :: Some4 (P4 X4 X4)) -> Just x === id' x + , QC.testProperty "Some1 (S1 X1 X1)" $ + QC.forAll QC.arbitrary $ \(x :: Some1 (S1 X1 X1)) -> Just x === id' x + , QC.testProperty "Some2 (S2 X2 X2)" $ + QC.forAll QC.arbitrary $ \(x :: Some2 (S2 X2 X2)) -> Just x === id' x + , QC.testProperty "Some3 (S3 X3 X3)" $ + QC.forAll QC.arbitrary $ \(x :: Some3 (S3 X3 X3)) -> Just x === id' x + , QC.testProperty "Some4 (S4 X4 X4)" $ + QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> Just x === id' x ] tt_nfdata :: Tasty.TestTree tt_nfdata = Tasty.testGroup "NFData" - [ QC.testProperty "Some1" $ - QC.forAll QC.arbitrary $ \(x :: Some1 Foo1) -> () === rnf x - , QC.testProperty "Some2" $ - QC.forAll QC.arbitrary $ \(x :: Some2 Foo2) -> () === rnf x - , QC.testProperty "Some3" $ - QC.forAll QC.arbitrary $ \(x :: Some3 Foo3) -> () === rnf x - , QC.testProperty "Some4" $ - QC.forAll QC.arbitrary $ \(x :: Some4 Foo4) -> () === rnf x + [ QC.testProperty "Some1 X1" $ + QC.forAll QC.arbitrary $ \(x :: Some1 X1) -> () === rnf x + , QC.testProperty "Some2 X2" $ + QC.forAll QC.arbitrary $ \(x :: Some2 X2) -> () === rnf x + , QC.testProperty "Some3 X3" $ + QC.forAll QC.arbitrary $ \(x :: Some3 X3) -> () === rnf x + , QC.testProperty "Some4 X4" $ + QC.forAll QC.arbitrary $ \(x :: Some4 X4) -> () === rnf x + , QC.testProperty "Some1 (P1 X1 X1)" $ + QC.forAll QC.arbitrary $ \(x :: Some1 (P1 X1 X1)) -> () === rnf x + , QC.testProperty "Some2 (P2 X2 X2)" $ + QC.forAll QC.arbitrary $ \(x :: Some2 (P2 X2 X2)) -> () === rnf x + , QC.testProperty "Some3 (P3 X3 X3)" $ + QC.forAll QC.arbitrary $ \(x :: Some3 (P3 X3 X3)) -> () === rnf x + , QC.testProperty "Some4 (P4 X4 X4)" $ + QC.forAll QC.arbitrary $ \(x :: Some4 (P4 X4 X4)) -> () === rnf x + , QC.testProperty "Some1 (S1 X1 X1)" $ + QC.forAll QC.arbitrary $ \(x :: Some1 (S1 X1 X1)) -> () === rnf x + , QC.testProperty "Some2 (S2 X2 X2)" $ + QC.forAll QC.arbitrary $ \(x :: Some2 (S2 X2 X2)) -> () === rnf x + , QC.testProperty "Some3 (S3 X3 X3)" $ + QC.forAll QC.arbitrary $ \(x :: Some3 (S3 X3 X3)) -> () === rnf x + , QC.testProperty "Some4 (S4 X4 X4)" $ + QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> () === rnf x ] tt_hashable :: Tasty.TestTree tt_hashable = Tasty.testGroup "Hashable" - [ QC.testProperty "Some1" $ - QC.forAll QC.arbitrary $ \(x :: Some1 Foo1) -> () === (hash x `seq` ()) - , QC.testProperty "Some2" $ - QC.forAll QC.arbitrary $ \(x :: Some2 Foo2) -> () === (hash x `seq` ()) - , QC.testProperty "Some3" $ - QC.forAll QC.arbitrary $ \(x :: Some3 Foo3) -> () === (hash x `seq` ()) - , QC.testProperty "Some4" $ - QC.forAll QC.arbitrary $ \(x :: Some4 Foo4) -> () === (hash x `seq` ()) + [ QC.testProperty "Some1 X1" $ + QC.forAll QC.arbitrary $ \(x :: Some1 X1) -> () === (hash x `seq` ()) + , QC.testProperty "Some2 X2" $ + QC.forAll QC.arbitrary $ \(x :: Some2 X2) -> () === (hash x `seq` ()) + , QC.testProperty "Some3 X3" $ + QC.forAll QC.arbitrary $ \(x :: Some3 X3) -> () === (hash x `seq` ()) + , QC.testProperty "Some4 X4" $ + QC.forAll QC.arbitrary $ \(x :: Some4 X4) -> () === (hash x `seq` ()) + , QC.testProperty "Some1 (P1 X1 X1)" $ + QC.forAll QC.arbitrary $ \(x :: Some1 (P1 X1 X1)) -> () === (hash x `seq` ()) + , QC.testProperty "Some2 (P2 X2 X2)" $ + QC.forAll QC.arbitrary $ \(x :: Some2 (P2 X2 X2)) -> () === (hash x `seq` ()) + , QC.testProperty "Some3 (P3 X3 X3)" $ + QC.forAll QC.arbitrary $ \(x :: Some3 (P3 X3 X3)) -> () === (hash x `seq` ()) + , QC.testProperty "Some4 (P4 X4 X4)" $ + QC.forAll QC.arbitrary $ \(x :: Some4 (P4 X4 X4)) -> () === (hash x `seq` ()) + , QC.testProperty "Some1 (S1 X1 X1)" $ + QC.forAll QC.arbitrary $ \(x :: Some1 (S1 X1 X1)) -> () === (hash x `seq` ()) + , QC.testProperty "Some2 (S2 X2 X2)" $ + QC.forAll QC.arbitrary $ \(x :: Some2 (S2 X2 X2)) -> () === (hash x `seq` ()) + , QC.testProperty "Some3 (S3 X3 X3)" $ + QC.forAll QC.arbitrary $ \(x :: Some3 (S3 X3 X3)) -> () === (hash x `seq` ()) + , QC.testProperty "Some4 (S4 X4 X4)" $ + QC.forAll QC.arbitrary $ \(x :: Some4 (S4 X4 X4)) -> () === (hash x `seq` ()) ] -------------------------------------------------------------------------------- +id_show_read :: (Show a, Read a) => a -> Maybe a +id_show_read = readMaybe . show + id_generic :: G.Generic a => a -> Maybe a id_generic = Just . G.to . G.from @@ -107,121 +168,128 @@ Left _ -> Nothing Right a' -> Just a' +id_binary :: Bin.Binary a => a -> Maybe a +id_binary = \a -> + case Bin.decodeOrFail (Bin.encode a) of + Right (z,_,a') | BSL.null z -> Just a' + _ -> Nothing + +id_cereal :: Cer.Serialize a => a -> Maybe a +id_cereal = \a -> + case Cer.decodeLazy (Cer.encodeLazy 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 Right (z,_,a') | BSL.null z -> Just a' _ -> Nothing +id_cereal_to_bytes :: (Cer.Serialize a, Bytes.Serial a) => a -> Maybe a +id_cereal_to_bytes = \a -> + case Bytes.runGetS Bytes.deserialize (Cer.encode a) of + Left _ -> Nothing + Right a' -> Just a' + id_binary_to_cereal :: (Bin.Binary a, Cer.Serialize a) => a -> Maybe a id_binary_to_cereal = \a -> case Cer.decodeLazy (Bin.encode a) of Right a' -> Just a' Left _ -> Nothing +id_binary_to_bytes :: (Bin.Binary a, Bytes.Serial a) => a -> Maybe a +id_binary_to_bytes = \a -> + case Bytes.runGetS Bytes.deserialize (BSL.toStrict (Bin.encode a)) of + Left _ -> Nothing + Right a' -> Just a' + +id_bytes_to_binary :: (Bytes.Serial a, Bin.Binary a) => a -> Maybe a +id_bytes_to_binary = \a -> + case Bin.decodeOrFail (Bytes.runPutL (Bytes.serialize a)) of + Right (z,_,a') | BSL.null z -> Just a' + _ -> Nothing + +id_bytes_to_cereal :: (Bytes.Serial a, Cer.Serialize a) => a -> Maybe a +id_bytes_to_cereal = \a -> + case Cer.decodeLazy (Bytes.runPutL (Bytes.serialize a)) of + Right a' -> Just a' + Left _ -> Nothing + -------------------------------------------------------------------------------- -data family Foo1 :: Bool -> Type -data instance Foo1 'False = F1 | F2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo1 'True = T1 | T2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) +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 family Foo2 :: Bool -> Bool -> Type -data instance Foo2 'False 'False = FF1 | FF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo2 'False 'True = FT1 | FT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo2 'True 'False = TF1 | TF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo2 'True 'True = TT1 | TT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, 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 family Foo3 :: Bool -> Bool -> Bool -> Type -data instance Foo3 'False 'False 'False = FFF1 | FFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo3 'False 'False 'True = FFT1 | FFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo3 'False 'True 'False = FTF1 | FTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo3 'False 'True 'True = FTT1 | FTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo3 'True 'False 'False = TFF1 | TFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo3 'True 'False 'True = TFT1 | TFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo3 'True 'True 'False = TTF1 | TTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo3 'True 'True 'True = TTT1 | TTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, 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 family Foo4 :: Bool -> Bool -> Bool -> Bool -> Type -data instance Foo4 'False 'False 'False 'False = FFFF1 | FFFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'False 'False 'False 'True = FFFT1 | FFFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'False 'False 'True 'False = FFTF1 | FFTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'False 'False 'True 'True = FFTT1 | FFTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'False 'True 'False 'False = FTFF1 | FTFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'False 'True 'False 'True = FTFT1 | FTFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'False 'True 'True 'False = FTTF1 | FTTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'False 'True 'True 'True = FTTT1 | FTTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'True 'False 'False 'False = TFFF1 | TFFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'True 'False 'False 'True = TFFT1 | TFFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'True 'False 'True 'False = TFTF1 | TFTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'True 'False 'True 'True = TFTT1 | TFTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'True 'True 'False 'False = TTFF1 | TTFF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'True 'True 'False 'True = TTFT1 | TTFT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'True 'True 'True 'False = TTTF1 | TTTF2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, NFData, Hashable) -data instance Foo4 'True 'True 'True 'True = TTTT1 | TTTT2 Int deriving (Eq, Show, G.Generic, Aeson.FromJSON, Aeson.ToJSON, Bytes.Serial, 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) -------------------------------------------------------------------------------- -- Arbitrary instances -instance QC.Arbitrary (Foo1 'False) where - arbitrary = QC.oneof [ pure F1, F2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo1 'True) where - arbitrary = QC.oneof [ pure T1, T2 <$> QC.arbitrary ] +instance QC.Arbitrary (X1 'False) where arbitrary = QC.oneof [ pure XF1, fmap XF2 QC.arbitrary ] +instance QC.Arbitrary (X1 'True) where arbitrary = QC.oneof [ pure XT1, fmap XT2 QC.arbitrary ] -instance QC.Arbitrary (Foo2 'False 'False) where - arbitrary = QC.oneof [ pure FF1, FF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo2 'False 'True) where - arbitrary = QC.oneof [ pure FT1, FT2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo2 'True 'False) where - arbitrary = QC.oneof [ pure TF1, TF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo2 'True 'True) where - arbitrary = QC.oneof [ pure TT1, TT2 <$> QC.arbitrary ] +instance QC.Arbitrary (X2 'False 'False) where arbitrary = QC.oneof [ pure XFF1, fmap XFF2 QC.arbitrary ] +instance QC.Arbitrary (X2 'False 'True) where arbitrary = QC.oneof [ pure XFT1, fmap XFT2 QC.arbitrary ] +instance QC.Arbitrary (X2 'True 'False) where arbitrary = QC.oneof [ pure XTF1, fmap XTF2 QC.arbitrary ] +instance QC.Arbitrary (X2 'True 'True) where arbitrary = QC.oneof [ pure XTT1, fmap XTT2 QC.arbitrary ] -instance QC.Arbitrary (Foo3 'False 'False 'False) where - arbitrary = QC.oneof [ pure FFF1, FFF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo3 'False 'False 'True) where - arbitrary = QC.oneof [ pure FFT1, FFT2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo3 'False 'True 'False) where - arbitrary = QC.oneof [ pure FTF1, FTF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo3 'False 'True 'True) where - arbitrary = QC.oneof [ pure FTT1, FTT2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo3 'True 'False 'False) where - arbitrary = QC.oneof [ pure TFF1, TFF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo3 'True 'False 'True) where - arbitrary = QC.oneof [ pure TFT1, TFT2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo3 'True 'True 'False) where - arbitrary = QC.oneof [ pure TTF1, TTF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo3 'True 'True 'True) where - arbitrary = QC.oneof [ pure TTT1, TTT2 <$> QC.arbitrary ] +instance QC.Arbitrary (X3 'False 'False 'False) where arbitrary = QC.oneof [ pure XFFF1, fmap XFFF2 QC.arbitrary ] +instance QC.Arbitrary (X3 'False 'False 'True) where arbitrary = QC.oneof [ pure XFFT1, fmap XFFT2 QC.arbitrary ] +instance QC.Arbitrary (X3 'False 'True 'False) where arbitrary = QC.oneof [ pure XFTF1, fmap XFTF2 QC.arbitrary ] +instance QC.Arbitrary (X3 'False 'True 'True) where arbitrary = QC.oneof [ pure XFTT1, fmap XFTT2 QC.arbitrary ] +instance QC.Arbitrary (X3 'True 'False 'False) where arbitrary = QC.oneof [ pure XTFF1, fmap XTFF2 QC.arbitrary ] +instance QC.Arbitrary (X3 'True 'False 'True) where arbitrary = QC.oneof [ pure XTFT1, fmap XTFT2 QC.arbitrary ] +instance QC.Arbitrary (X3 'True 'True 'False) where arbitrary = QC.oneof [ pure XTTF1, fmap XTTF2 QC.arbitrary ] +instance QC.Arbitrary (X3 'True 'True 'True) where arbitrary = QC.oneof [ pure XTTT1, fmap XTTT2 QC.arbitrary ] -instance QC.Arbitrary (Foo4 'False 'False 'False 'False) where - arbitrary = QC.oneof [ pure FFFF1, FFFF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'False 'False 'False 'True) where - arbitrary = QC.oneof [ pure FFFT1, FFFT2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'False 'False 'True 'False) where - arbitrary = QC.oneof [ pure FFTF1, FFTF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'False 'False 'True 'True) where - arbitrary = QC.oneof [ pure FFTT1, FFTT2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'False 'True 'False 'False) where - arbitrary = QC.oneof [ pure FTFF1, FTFF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'False 'True 'False 'True) where - arbitrary = QC.oneof [ pure FTFT1, FTFT2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'False 'True 'True 'False) where - arbitrary = QC.oneof [ pure FTTF1, FTTF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'False 'True 'True 'True) where - arbitrary = QC.oneof [ pure FTTT1, FTTT2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'True 'False 'False 'False) where - arbitrary = QC.oneof [ pure TFFF1, TFFF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'True 'False 'False 'True) where - arbitrary = QC.oneof [ pure TFFT1, TFFT2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'True 'False 'True 'False) where - arbitrary = QC.oneof [ pure TFTF1, TFTF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'True 'False 'True 'True) where - arbitrary = QC.oneof [ pure TFTT1, TFTT2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'True 'True 'False 'False) where - arbitrary = QC.oneof [ pure TTFF1, TTFF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'True 'True 'False 'True) where - arbitrary = QC.oneof [ pure TTFT1, TTFT2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'True 'True 'True 'False) where - arbitrary = QC.oneof [ pure TTTF1, TTTF2 <$> QC.arbitrary ] -instance QC.Arbitrary (Foo4 'True 'True 'True 'True) where - arbitrary = QC.oneof [ pure TTTT1, TTTT2 <$> QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'False 'False 'False) where arbitrary = QC.oneof [ pure XFFFF1, fmap XFFFF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'False 'False 'True) where arbitrary = QC.oneof [ pure XFFFT1, fmap XFFFT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'False 'True 'False) where arbitrary = QC.oneof [ pure XFFTF1, fmap XFFTF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'False 'True 'True) where arbitrary = QC.oneof [ pure XFFTT1, fmap XFFTT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'True 'False 'False) where arbitrary = QC.oneof [ pure XFTFF1, fmap XFTFF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'True 'False 'True) where arbitrary = QC.oneof [ pure XFTFT1, fmap XFTFT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'True 'True 'False) where arbitrary = QC.oneof [ pure XFTTF1, fmap XFTTF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'False 'True 'True 'True) where arbitrary = QC.oneof [ pure XFTTT1, fmap XFTTT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'False 'False 'False) where arbitrary = QC.oneof [ pure XTFFF1, fmap XTFFF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'False 'False 'True) where arbitrary = QC.oneof [ pure XTFFT1, fmap XTFFT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'False 'True 'False) where arbitrary = QC.oneof [ pure XTFTF1, fmap XTFTF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'False 'True 'True) where arbitrary = QC.oneof [ pure XTFTT1, fmap XTFTT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'True 'False 'False) where arbitrary = QC.oneof [ pure XTTFF1, fmap XTTFF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'True 'False 'True) where arbitrary = QC.oneof [ pure XTTFT1, fmap XTTFT2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'True 'True 'False) where arbitrary = QC.oneof [ pure XTTTF1, fmap XTTTF2 QC.arbitrary ] +instance QC.Arbitrary (X4 'True 'True 'True 'True) where arbitrary = QC.oneof [ pure XTTTT1, fmap XTTTT2 QC.arbitrary ] +