exinst (empty) → 0.1
raw patch · 8 files changed
+1171/−0 lines, 8 filesdep +basedep +constraintsdep +singletonssetup-changed
Dependencies added: base, constraints, singletons
Files
- CHANGELOG.md +3/−0
- LICENSE.txt +30/−0
- README.md +568/−0
- Setup.hs +2/−0
- exinst.cabal +30/−0
- src/lib/Exinst/Instances/Base.hs +278/−0
- src/lib/Exinst/Singletons.hs +231/−0
- src/lib/Exinst/Singletons/Internal.hs +29/−0
+ CHANGELOG.md view
@@ -0,0 +1,3 @@+# Version 0.1++* Initial release.
+ LICENSE.txt view
@@ -0,0 +1,30 @@+Copyright (c) 2015, Renzo Carbonara++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Renzo Carbonara nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,568 @@+# 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:++> TODO: check language extensions needed for 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` (which could have been derived+automatically, too).++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. That is, we can+have `[Receptacle 'Small]` and `[Receptacle 'Big]`, but we can't have+`[Receptacle]`. 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.Singletons (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.Singletons.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`.++As of this writing, we can find some ready-made instances for `Some1`, `Some2`,+`Some3` and `Some4` in the following modules, which you need to import so as to+bring to scope the desired instances at their usage site:++* Package `exinst`, module `Exinst.Instances.Base`: Instances for various+ type-classes found in the `base` package: `Eq`, `Ord`, `Show`.++* Package `exinst-aeson`, module `Exinst.Instances.Aeson`: Instances for+ `FromJSON` and `ToJSON` from the `aeson` package.++* Package `exinst-bytes`, module `Exinst.Instances.Bytes`: Instances for+ `Serial` from the `bytes` package.++* Package `exinst-hashable`, module `Exinst.Instances.Hashable`: Instances for+ `Hashable` from the `hashable` package.++* Package `exinst-deepseq`, module `Exinst.Instances.DeepSeq`: Instances for+ `NFData` from the `deepseq` 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.++> TODO: Have something similar to `Dict1` and friends for working with+> non-singleton types, possibly integrating with 'Data.Constraint.Forall.ForallT'+> if it made sense to do so.++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.Singletons (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`.+++# Related work on Generic instances for GADTs++One of the most appealing applications of `exinst` is to reduce the boilerplate+associated with manually writing instances for existentialized GADTs. However,+quite often, writing instances for said GADTs on its own is very cumbersome+due to the lack of generic instance deriving mechanisms for GADTs. There exists,+however, at the time of this writing, at least one library able to derive+generic representations for some GADTs using TH:+[`instant-generics`](https://hackage.haskell.org/package/instant-generics).++Combining [`instant-generics`](https://hackage.haskell.org/package/instant-generics) (and+[`instant-aeson`](https://hackage.haskell.org/package/instant-aeson),+[`instant-hashable`](https://hackage.haskell.org/package/instant-hashable),+[`instant-bytes`](https://hackage.haskell.org/package/instant-bytes) and+[`instant-deepseq`](https://hackage.haskell.org/package/instant-deepseq))+with [`exinst-generics`](https://hackage.haskell.org/package/exinst-generics) (and+[`exinst-aeson`](https://hackage.haskell.org/package/exinst-aeson),+[`exinst-hashable`](https://hackage.haskell.org/package/exinst-hashable),+[`exinst-bytes`](https://hackage.haskell.org/package/exinst-bytes) and+[`exinst-deepseq`](https://hackage.haskell.org/package/exinst-deepseq)),+you can reduce a lot of the boilerplate associated with working with GADTs, in+particular when it comes to the serialization and deserialization of them (i.e.,+`Show` and `Read`, or `ToJSON` and `FromJSON`) or puting GADTs in monomorphic+containers (i.e., `[]` or `HashMap`), which become straightforward things to do+once you are able able to both generically derive the instances for your GADT+and then existentialize away the type-index while keeping the underlying+instances available.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ exinst.cabal view
@@ -0,0 +1,30 @@+name: exinst+version: 0.1+author: Renzo Carbonara+maintainer: renzoλcarbonara.com.ar+copyright: Renzo Carbonara 2015+license: BSD3+license-file: LICENSE.txt+extra-source-files: README.md CHANGELOG.md+category: Data+build-type: Simple+cabal-version: >=1.18+synopsis: Derive instances for your existential types.+homepage: https://github.com/k0001/exinst+bug-reports: https://github.com/k0001/exinst/issues+ ++library+ hs-source-dirs: src/lib+ default-language: Haskell2010+ exposed-modules:+ Exinst.Singletons+ Exinst.Instances.Base+ other-modules:+ Exinst.Singletons.Internal+ build-depends:+ base >=4.7 && <4.9+ , constraints >=0.4 && <0.5+ , singletons >=1.1 && <1.2+ ghcjs-options: -Wall -O3+ ghc-options: -Wall -O2
+ src/lib/Exinst/Instances/Base.hs view
@@ -0,0 +1,278 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | This module exports 'Show', 'Eq' and 'Ord' instances for 'Some1',+-- 'Some2', 'Some3' and 'Some4' from "Exinst.Singletons", provided situable+-- 'Dict1', 'Dict2', 'Dict3' and 'Dict4' instances are available.+--+-- See the README file for more general documentation: https://hackage.haskell.org/package/exinst#readme+module Exinst.Instances.Base () where++import Data.Constraint+import Data.Singletons+import Data.Singletons.Decide+import Data.Singletons.Types+import Exinst.Singletons+import Prelude++--------------------------------------------------------------------------------++-- 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 -> *)+ . ( SingKind ('KProxy :: KProxy k1)+ , Show (DemoteRep ('KProxy :: KProxy k1))+ , Dict1 Show f1+ ) => Show (Some1 f1)+ where+ {-# INLINABLE showsPrec #-}+ showsPrec n = \some1x -> withSome1Sing some1x $ \sa1 (x :: f1 a1) ->+ case dict1 sa1 :: Dict (Show (f1 a1)) of+ Dict -> showsPrec n (Some1 (fromSing sa1) x)++instance forall (f2 :: k2 -> k1 -> *)+ . ( SingKind ('KProxy :: KProxy k2)+ , SingKind ('KProxy :: KProxy k1)+ , Show (DemoteRep ('KProxy :: KProxy k2))+ , Show (DemoteRep ('KProxy :: KProxy k1))+ , Dict2 Show f2+ ) => Show (Some2 f2)+ where+ {-# INLINABLE showsPrec #-}+ showsPrec n = \some2x -> withSome2Sing some2x $ \sa2 sa1 (x :: f2 a2 a1) ->+ case dict2 sa2 sa1 :: Dict (Show (f2 a2 a1)) of+ Dict -> showsPrec n (Some2 (fromSing sa2) (fromSing sa1) x)++instance forall (f3 :: k3 -> k2 -> k1 -> *)+ . ( SingKind ('KProxy :: KProxy k3)+ , SingKind ('KProxy :: KProxy k2)+ , SingKind ('KProxy :: KProxy k1)+ , Show (DemoteRep ('KProxy :: KProxy k3))+ , Show (DemoteRep ('KProxy :: KProxy k2))+ , Show (DemoteRep ('KProxy :: KProxy k1))+ , Dict3 Show f3+ ) => Show (Some3 f3)+ 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+ Dict -> showsPrec n (Some3 (fromSing sa3) (fromSing sa2) (fromSing sa1) x)++instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)+ . ( SingKind ('KProxy :: KProxy k4)+ , SingKind ('KProxy :: KProxy k3)+ , SingKind ('KProxy :: KProxy k2)+ , SingKind ('KProxy :: KProxy k1)+ , Show (DemoteRep ('KProxy :: KProxy k4))+ , Show (DemoteRep ('KProxy :: KProxy k3))+ , Show (DemoteRep ('KProxy :: KProxy k2))+ , Show (DemoteRep ('KProxy :: KProxy k1))+ , Dict4 Show f4+ ) => Show (Some4 f4)+ 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+ Dict -> showsPrec n (Some4 (fromSing sa4) (fromSing sa3)+ (fromSing sa2) (fromSing sa1) x)++--------------------------------------------------------------------------------+-- Read++--------------------------------------------------------------------------------+-- Eq++instance forall (f1 :: k1 -> *)+ . ( SingKind ('KProxy :: KProxy k1)+ , SDecide ('KProxy :: KProxy k1)+ , Dict1 Eq f1+ ) => Eq (Some1 f1)+ 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)++instance forall (f2 :: k2 -> k1 -> *)+ . ( SingKind ('KProxy :: KProxy k2)+ , SingKind ('KProxy :: KProxy k1)+ , SDecide ('KProxy :: KProxy k2)+ , SDecide ('KProxy :: KProxy k1)+ , Dict2 Eq f2+ ) => Eq (Some2 f2)+ where+ {-# INLINABLE (==) #-}+ (==) = \som2x som2y -> + withSome2Sing som2x $ \sa2x sa1x (x :: f2 a2x a1x) -> + withSome2Sing som2y $ \sa2y sa1y (y :: f2 a2y a1y) -> + maybe False id $ do+ Refl <- testEquality sa2x sa2y+ Refl <- testEquality sa1x sa1y+ case dict2 sa2x sa1x :: Dict (Eq (f2 a2x a1x)) of+ Dict -> Just (x == y)++instance forall (f3 :: k3 -> k2 -> k1 -> *)+ . ( SingKind ('KProxy :: KProxy k3)+ , SingKind ('KProxy :: KProxy k2)+ , SingKind ('KProxy :: KProxy k1)+ , SDecide ('KProxy :: KProxy k3)+ , SDecide ('KProxy :: KProxy k2)+ , SDecide ('KProxy :: KProxy k1)+ , Dict3 Eq f3+ ) => Eq (Some3 f3)+ where+ {-# INLINABLE (==) #-}+ (==) = \som3x som3y -> + withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f3 a3x a2x a1x) -> + withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f3 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+ Dict -> Just (x == y)++instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)+ . ( SingKind ('KProxy :: KProxy k4)+ , SingKind ('KProxy :: KProxy k3)+ , SingKind ('KProxy :: KProxy k2)+ , SingKind ('KProxy :: KProxy k1)+ , SDecide ('KProxy :: KProxy k4)+ , SDecide ('KProxy :: KProxy k3)+ , SDecide ('KProxy :: KProxy k2)+ , SDecide ('KProxy :: KProxy k1)+ , Dict4 Eq f4+ ) => Eq (Some4 f4)+ 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) -> + 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+ Dict -> Just (x == y)++--------------------------------------------------------------------------------+-- Ord++instance forall (f1 :: k1 -> *)+ . ( SingKind ('KProxy :: KProxy k1)+ , SDecide ('KProxy :: KProxy k1)+ , Ord (DemoteRep ('KProxy :: KProxy k1))+ , Dict1 Ord f1+ , Eq (Some1 f1)+ ) => Ord (Some1 f1)+ where+ {-# INLINABLE compare #-}+ compare = \som1x som1y -> + withSome1Sing som1x $ \sa1x (x :: f1 a1x) -> + withSome1Sing som1y $ \sa1y (y :: f1 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+ Dict -> Just (compare x y)++instance forall (f2 :: k2 -> k1 -> *)+ . ( SingKind ('KProxy :: KProxy k2)+ , SingKind ('KProxy :: KProxy k1)+ , SDecide ('KProxy :: KProxy k2)+ , SDecide ('KProxy :: KProxy k1)+ , Ord (DemoteRep ('KProxy :: KProxy k2))+ , Ord (DemoteRep ('KProxy :: KProxy k1))+ , Dict2 Ord f2+ , Eq (Some2 f2)+ ) => Ord (Some2 f2)+ where+ {-# INLINABLE compare #-}+ compare = \som2x som2y -> + withSome2Sing som2x $ \sa2x sa1x (x :: f2 a2x a1x) -> + withSome2Sing som2y $ \sa2y sa1y (y :: f2 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+ Dict -> Just (compare x y)++instance forall (f3 :: k3 -> k2 -> k1 -> *)+ . ( SingKind ('KProxy :: KProxy k3)+ , SingKind ('KProxy :: KProxy k2)+ , SingKind ('KProxy :: KProxy k1)+ , SDecide ('KProxy :: KProxy k3)+ , SDecide ('KProxy :: KProxy k2)+ , SDecide ('KProxy :: KProxy k1)+ , Ord (DemoteRep ('KProxy :: KProxy k3))+ , Ord (DemoteRep ('KProxy :: KProxy k2))+ , Ord (DemoteRep ('KProxy :: KProxy k1))+ , Dict3 Ord f3+ , Eq (Some3 f3)+ ) => Ord (Some3 f3)+ 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) -> + let termCompare = compare+ (fromSing sa3x, fromSing sa2x, fromSing sa1x)+ (fromSing sa3y, fromSing sa2y, fromSing sa1y)+ in maybe termCompare id $ do+ Refl <- testEquality sa3x sa3y+ Refl <- testEquality sa2x sa2y+ Refl <- testEquality sa1x sa1y+ case dict3 sa3x sa2x sa1x :: Dict (Ord (f3 a3x a2x a1x)) of+ Dict -> Just (compare x y)++instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)+ . ( SingKind ('KProxy :: KProxy k4)+ , SingKind ('KProxy :: KProxy k3)+ , SingKind ('KProxy :: KProxy k2)+ , SingKind ('KProxy :: KProxy k1)+ , SDecide ('KProxy :: KProxy k4)+ , SDecide ('KProxy :: KProxy k3)+ , SDecide ('KProxy :: KProxy k2)+ , SDecide ('KProxy :: KProxy k1)+ , Ord (DemoteRep ('KProxy :: KProxy k4))+ , Ord (DemoteRep ('KProxy :: KProxy k3))+ , Ord (DemoteRep ('KProxy :: KProxy k2))+ , Ord (DemoteRep ('KProxy :: KProxy k1))+ , Dict4 Ord f4+ , Eq (Some4 f4)+ ) => Ord (Some4 f4)+ 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) -> + let termCompare = compare+ (fromSing sa4x, fromSing sa3x, fromSing sa2x, fromSing sa1x)+ (fromSing sa4y, fromSing sa3y, fromSing sa2y, fromSing sa1y)+ in maybe termCompare id $ do+ Refl <- testEquality sa4x sa4y+ Refl <- testEquality sa3x sa3y+ Refl <- testEquality sa2x sa2y+ Refl <- testEquality sa1x sa1y+ case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f4 a4x a3x a2x a1x)) of+ Dict -> Just (compare x y)+
+ src/lib/Exinst/Singletons.hs view
@@ -0,0 +1,231 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}++-- | See the README file for documentation: https://hackage.haskell.org/package/exinst#readme+module Exinst.Singletons+ ( -- * 1 type index+ Some1+ , some1+ , withSome1Sing+ , withSome1+ , fromSome1+ , Dict1(dict1)++ -- * 2 type indexes+ , Some2+ , some2+ , withSome2Sing+ , withSome2+ , fromSome2+ , Dict2(dict2)++ -- * 3 type indexes+ , Some3+ , some3+ , withSome3Sing+ , withSome3+ , fromSome3+ , Dict3(dict3)++ -- * 4 type indexes+ , Some4+ , some4+ , withSome4Sing+ , withSome4+ , fromSome4+ , Dict4(dict4)+ ) where++import Data.Constraint+import Data.Singletons+import Data.Singletons.Decide+import Data.Singletons.Types+import Prelude++import Exinst.Singletons.Internal++--------------------------------------------------------------------------------++some1+ :: forall (f1 :: k1 -> *) a1+ . SingI a1+ => f1 a1+ -> Some1 f1 -- ^+some1 = Some1 (sing :: Sing a1)+{-# INLINE some1 #-}++some2+ :: forall (f2 :: k2 -> k1 -> *) a2 a1+ . (SingI a2, SingI a1)+ => f2 a2 a1+ -> Some2 f2 -- ^+some2 = Some2 (sing :: Sing a2) (sing :: Sing a1)+{-# INLINE some2 #-}++some3+ :: forall (f3 :: k3 -> k2 -> k1 -> *) a3 a2 a1+ . (SingI a3, SingI a2, SingI a1)+ => f3 a3 a2 a1+ -> Some3 f3 -- ^+some3 = Some3 (sing :: Sing a3) (sing :: Sing a2) (sing :: Sing a1)+{-# INLINE some3 #-}++some4+ :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) a4 a3 a2 a1+ . (SingI a4, SingI a3, SingI a2, SingI a1)+ => f4 a4 a3 a2 a1+ -> Some4 f4 -- ^+some4 = Some4 (sing :: Sing a4) (sing :: Sing a3)+ (sing :: Sing a2) (sing :: Sing a1)+{-# INLINE some4 #-}++--------------------------------------------------------------------------------++withSome1+ :: forall (f1 :: k1 -> *) (r :: *)+ . Some1 f1+ -> (forall a1. SingI a1 => f1 a1 -> r)+ -> r -- ^+withSome1 (Some1 sa1 x) g = withSingI sa1 (g x)+{-# INLINABLE withSome1 #-}++withSome2+ :: forall (f2 :: k2 -> k1 -> *) (r :: *)+ . Some2 f2+ -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r)+ -> r -- ^+withSome2 (Some2 sa2 sa1 x) g = withSingI sa2 (withSingI sa1 (g x))+{-# INLINABLE withSome2 #-}++withSome3+ :: forall (f3 :: k3 -> k2 -> k1 -> *) (r :: *)+ . Some3 f3+ -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r)+ -> r -- ^+withSome3 (Some3 sa3 sa2 sa1 x) g =+ withSingI sa3 (withSingI sa2 (withSingI sa1 (g x)))+{-# INLINABLE withSome3 #-}++withSome4+ :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) (r :: *)+ . Some4 f4+ -> (forall a4 a3 a2 a1+ . (SingI a4, SingI a3, SingI a2, SingI a1)+ => f4 a4 a3 a2 a1 -> r)+ -> r -- ^+withSome4 (Some4 sa4 sa3 sa2 sa1 x) g =+ withSingI sa4 (withSingI sa3 (withSingI sa2 (withSingI sa1 (g x))))+{-# INLINABLE withSome4 #-}++--------------------------------------------------------------------------------++-- | Like 'withSome1', but takes an explicit 'Sing' instead of a 'SingI' instance.+withSome1Sing+ :: forall (f1 :: k1 -> *) (r :: *)+ . Some1 f1+ -> (forall a1. Sing a1 -> f1 a1 -> r)+ -> r -- ^+withSome1Sing (Some1 sa1 x) g = g sa1 x+{-# INLINABLE withSome1Sing #-}++-- | Like 'withSome2', but takes explicit 'Sing's instead of 'SingI' instances.+withSome2Sing+ :: forall (f2 :: k2 -> k1 -> *) (r :: *)+ . Some2 f2+ -> (forall a2 a1. Sing a2 -> Sing a1 -> f2 a2 a1 -> r)+ -> r -- ^+withSome2Sing (Some2 sa2 sa1 x) g = g sa2 sa1 x+{-# INLINABLE withSome2Sing #-}++-- | Like 'withSome3', but takes explicit 'Sing's instead of 'SingI' instances.+withSome3Sing+ :: forall (f3 :: k3 -> k2 -> k1 -> *) (r :: *)+ . Some3 f3+ -> (forall a3 a2 a1. Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)+ -> r -- ^+withSome3Sing (Some3 sa3 sa2 sa1 x) g = g sa3 sa2 sa1 x+{-# INLINABLE withSome3Sing #-}++-- | Like 'withSome4', but takes explicit 'Sing's instead of 'SingI' instances.+withSome4Sing+ :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) (r :: *)+ . Some4 f4+ -> (forall a4 a3 a2 a1+ . Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)+ -> r -- ^+withSome4Sing (Some4 sa4 sa3 sa2 sa1 x) g = g sa4 sa3 sa2 sa1 x+{-# INLINABLE withSome4Sing #-}++--------------------------------------------------------------------------------++fromSome1+ :: forall (f1 :: k1 -> *) a1+ . (SingI a1, SDecide ('KProxy :: KProxy k1))+ => Some1 f1+ -> Maybe (f1 a1) -- ^+fromSome1 = \(Some1 sa1' x) -> do+ Refl <- testEquality sa1' (sing :: Sing a1)+ return x+{-# INLINABLE fromSome1 #-}++fromSome2+ :: forall (f2 :: k2 -> k1 -> *) a2 a1+ . ( SingI a2, SDecide ('KProxy :: KProxy k2)+ , SingI a1, SDecide ('KProxy :: KProxy k1))+ => Some2 f2+ -> Maybe (f2 a2 a1) -- ^+fromSome2 = \(Some2 sa2' sa1' x) -> do+ Refl <- testEquality sa2' (sing :: Sing a2)+ Refl <- testEquality sa1' (sing :: Sing a1)+ return x+{-# INLINABLE fromSome2 #-}++fromSome3+ :: forall (f3 :: k3 -> k2 -> k1 -> *) a3 a2 a1+ . ( SingI a3, SDecide ('KProxy :: KProxy k3)+ , SingI a2, SDecide ('KProxy :: KProxy k2)+ , SingI a1, SDecide ('KProxy :: KProxy k1))+ => Some3 f3+ -> Maybe (f3 a3 a2 a1) -- ^+fromSome3 = \(Some3 sa3' sa2' sa1' x) -> do+ Refl <- testEquality sa3' (sing :: Sing a3)+ Refl <- testEquality sa2' (sing :: Sing a2)+ Refl <- testEquality sa1' (sing :: Sing a1)+ return x+{-# INLINABLE fromSome3 #-}++fromSome4+ :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) a4 a3 a2 a1+ . ( SingI a4, SDecide ('KProxy :: KProxy k4)+ , SingI a3, SDecide ('KProxy :: KProxy k3)+ , SingI a2, SDecide ('KProxy :: KProxy k2)+ , SingI a1, SDecide ('KProxy :: KProxy k1))+ => Some4 f4+ -> Maybe (f4 a4 a3 a2 a1) -- ^+fromSome4 = \(Some4 sa4' sa3' sa2' sa1' x) -> do+ Refl <- testEquality sa4' (sing :: Sing a4)+ Refl <- testEquality sa3' (sing :: Sing a3)+ Refl <- testEquality sa2' (sing :: Sing a2)+ Refl <- testEquality sa1' (sing :: Sing a1)+ return x+{-# INLINABLE fromSome4 #-}++--------------------------------------------------------------------------------++class Dict1 (c :: * -> Constraint) (f1 :: k1 -> *) where+ dict1 :: Sing a1 -> Dict (c (f1 a1))++class Dict2 (c :: * -> Constraint) (f2 :: k2 -> k1 -> *) where+ dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))++class Dict3 (c :: * -> Constraint) (f3 :: k3 -> k2 -> k1 -> *) where+ dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))++class Dict4 (c :: * -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> *) where+ dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
+ src/lib/Exinst/Singletons/Internal.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE PolyKinds #-}++-- | This is an internal module, do not import it directly. Import+-- "Exinst.Singletons" instead.+module Exinst.Singletons.Internal+ ( Some1(..)+ , Some2(..)+ , Some3(..)+ , Some4(..)+ ) where++import Data.Singletons (Sing)++--------------------------------------------------------------------------------++data Some1 (f1 :: k1 -> *) = forall a1.+ Some1 !(Sing a1) (f1 a1)++data Some2 (f2 :: k2 -> k1 -> *) = forall a2 a1.+ Some2 !(Sing a2) !(Sing a1) (f2 a2 a1)++data Some3 (f3 :: k3 -> k2 -> k1 -> *) = forall a3 a2 a1.+ Some3 !(Sing a3) !(Sing a2) !(Sing a1) (f3 a3 a2 a1)++data Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> *) = forall a4 a3 a2 a1.+ Some4 !(Sing a4) !(Sing a3) !(Sing a2) !(Sing a1) (f4 a4 a3 a2 a1)++--------------------------------------------------------------------------------