kind-generics (empty) → 0.1.0.0
raw patch · 8 files changed
+690/−0 lines, 8 filesdep +basedep +kind-applysetup-changed
Dependencies added: base, kind-apply
Files
- LICENSE +30/−0
- README.md +249/−0
- Setup.hs +2/−0
- kind-generics.cabal +30/−0
- src/Generics/Kind.hs +162/−0
- src/Generics/Kind/Derive/Eq.hs +48/−0
- src/Generics/Kind/Derive/Functor.hs +105/−0
- src/Generics/Kind/Examples.hs +64/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2018, Alejandro Serrano++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 Alejandro Serrano 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,249 @@+# `kind-generics`: generic programming for arbitrary kinds and GADTs++Data type-generic programming in Haskell is restricted to types of kind `*` (by using `Generic`) or `* -> *` (by using `Generic1`). This works fine for implementing generic equality or generic printing, notions which are applied to types of kind `*`. But what about having a generic `Bifunctor` or `Contravariant`? We need to extend our language for describing data types to other kinds -- hopefully without having to introduce `Generic2`, `Generic3`, and so on.++The language for describing data types in `GHC.Generics` is also quite restricted. In particular, it can only describe algebraic data types, not the full extent of GADTs. It turns out that both problems are related: if you want to describe a constructor of the form `forall a. blah`, then `blah` must be a data type which takes one additional type variable. As a result, we need to enlarge and shrink the kind at will.++This library, `kind-generics`, provides a new type class `GenericK` and a set of additional functors `F` (from *field*), `C` (from *constraint*), and `E` (from *existential*) which extend the language of `GHC.Generics`. We have put a lot of effort in coming with a simple programming experience, even though the implementation is full of type trickery.++## Short summary for simple data types++GHC has built-in support for data type-generic programming via its `GHC.Generics` module. In order to use those facilities, your data type must implement the `Generic` type class. Fortunately, GHC can automatically derive such instances for algebraic data types. For example:++```haskell+{-# language DeriveGeneric #-} -- this should be at the top of the file++data Tree a = Branch (Tree a) (Tree a) | Leaf a+ deriving Generic -- this is the magical line+```++From this `Generic` instance, `kind-generics` can derive another one for its very own `GenericK`. It needs one additional piece of information, though: the description of the data type in the enlarged language of descriptions. The reason for this is that `Generic` does not distinguish whether the type of a field mentions one of the type variables (`a` in this case) or not. But `GenericK` requires so.++Let us look at the `GenericK` instance for `Tree`:++```haskell+instance GenericK Tree (a :&&: LoT0) where+ type RepK Tree = (F (Tree :$: V0) :*: F (Tree :$: V0)) :+: (F V0)+```++In this case we have two constructors, separated by `(:+:)`. The first constructor has two fields, tied together by `(:*:)`. In the description of each field is where the difference with `GHC.Generics` enters the game: you need to describe *each* piece which makes us the type. In this case `Tree :$: V0` says that the type constructor `Tree` is applied to the first type variable. Type variables, in turn, are represented by zero-indexed `V0`, `V1`, and so on.++The other piece of information we need to give `GenericK` is how to separate the type constructor from its arguments. The first line of the instance always takes the name of the type, and then a *list of types* representing each of the arguments. In this case there is only one argument, and thus the list has only one element. In order to get better type inference you might also add the following declaration:++```haskell+instance Split (Tree a) Tree (a :&&: LoT0)+```++You can finally use the functionality from `kind-generics` and derive some type classes automatically:++```haskell+import Generics.Kind.Derive.Eq+import Generics.Kind.Derive.Functor++instance Eq a => Eq (Tree a) where+ (==) = geq'+instance Functor Tree where+ fmap = fmapDefault+```++## Type variables in a list: `LoT` and `(:@@:)`++Let us have a closer look at the definition of the `GenericK` type class. If you have been using other data type-generic programming libraries you might recognize `RepK` as the generalized version of `Rep`, which ties a data type with its description, and the pair of functions `fromK` and `toK` to go back and forth the original values and their generic counterparts.++```haskell+class GenericK (f :: k) (x :: LoT k) where+ type RepK f :: LoT k -> *+ fromK :: f :@@: x -> RepK f x+ toK :: RepK f x -> f :@@: x+```++But what are those `LoT` and `(:@@:)` which appear there? That is indeed the secret sauce which makes the whole `kind-generics` library work. The name `LoT` comes from *list of types*. It is a type-level version of a regular list, where the `(:)` constructor is replaced by `(:&&:)` and the empty list is represented by `LoT0`. For example:++```haskell+Int :&&: [Bool] :&&: LoT0 -- a list with two basic types+Int :&&: [] :&&: LoT0 -- type constructor may also appear+```++What can you do with such a list of types? You can pass them as type arguments to a type constructor. This is the role of `(:@@:)` (which you can pronounce *of*, or *application*). For example:++```haskell+Either :@@: (Int :&&: Bool :&&: LoT0) = Either Int Bool+Free :@@: ([] :&&: Int :&&: LoT0) = Free [] Int+Int :@@: LoT0 = Int+```++Wait, you cannot apply any list of types to any constructor! Something like `Maybe []` is rejected by the compiler, and so should we reject `Maybe ([] :&&: LoT0)`. To prevent such problems, the list of types is decorated with the *kinds* of all the types inside of it. Going back to the previous examples:++```haskell+Int :&&: [Bool] :&&: LoT0 :: LoT (* -> * -> *)+Int :&&: [] :&&: LoT0 :: LoT (* -> (* -> *) -> *)+```++The application operator `(:@@:)` only allows us to apply a list of types of kind `k` to types constructors of the same kind. The shared variable in the head of the type class enforces this invariant also in our generic descriptions.++### Helper classes: `GenericS`, `GenericF`, `GenericN`++If you want to turn a value into its generic representation, the `fromK` method of the `GenericK` class should be enough. Alas, that is a hard nut to crack for GHC's inference engine. Imagine you call `fromK (Left True)`: should it break the type `Either Bool a` into `Either :@@: (Bool :&&: a :&&: LoT0)`, or maybe into `Either Bool :@@: (a :&&: LoT0)`? In principle, it is possible that even *both* instances exist, although it does not make sense in the context of this library.++It turns out that the interface provided by `GenericK` is very helpful for those writing conversion from and to generic representations, but not so much for those using `fromK` and `toK`. For that reason, `kind-generics` provides three different extensions to `GenericK` depending on how much of the type you know:++* When the type is completely known and you have an instance for `Split` (which describes how to separate a type into its head and its type arguments), you should use `GenericS`. This is the most common scenario: for example, `fromS (Left True)` works as you may expect, using the `GenericK` instance for `Either`. This option also provides the closest experience to `GHC.Generics`.+* When you know the `f` in the `f :@@: x`, it is possible to use `GenericF`. In that case, you have to provide the head of the type using a type application. For example, `fromF @Either (Just True)`.+* A third option is to indicate *how many* arguments should go in the list of types `x` to generate `f :@@: x`. In the previous case, you might have also used `fromN @(S (S Z)) (Just True)`. Note that the length of the list of types is expressed as a unary number.++## Describing fields: the functor `F`++As mentioned in the introduction, `kind-generics` features a more expressive language to describe the types of the fields of data types. We call the description of a specific type an *atom*. The language of atoms reproduces the ways in which you can build a type in Haskell:++1. You can have a constant type `t`, which is represented by `Kon t`.+2. You can mention a variable, which is represented by `V0`, `V1`, and so on. For those interested in the internals, there is a general `Var v` where `v` is a type-level number. The library provides the synonyms for ergonomic reasons.+3. You can take two types `f` and `x` and apply one to the other, `f :@: x`.++For example, suppose the `a` is the name of the first type variable and `b` the name of the second. Here are the corresponding atoms:++```haskell+a -> V0+Maybe a -> Kon Maybe :@: V0+Either b a -> Kon Either :@: V1 :@: V0+b (Maybe a) -> V1 :@: (Kon Maybe :@: V0)+```++Since the `Kon f :@: x` pattern is very common, `kind-generics` also allows you to write it as simply `f :$: x`. The names `(:$:)` and `(:@:)` are supposed to resemble `(<$>)` and `(<*>)` from the `Applicative` type class.++The kind of an atom is described by two pieces of information, `Atom d k`. The first argument `d` specifies the amounf of variables that it uses. The second argument `k` tells you the kind of the type you obtain if you replace the variable markers `V0`, `V1`, ... by actual types. For example:++```haskell+V0 -> Atom (k -> ks) k+V1 :@: (Maybe :$: V0) -> Atom (* -> (* -> *) -> ks) (*)+```++In the first example, if you tell me the value of the variable `a` regardless of the kind `k`, the library can build a type of kind `k`. In the second example, the usage requires the first variable to be a ground type, and the second one to be a one-parameter type constructor. If you give those types, the library can build a type of kind `*`.++This operation we have just described is embodied by the `Ty` type family. A call looks like `Ty atom lot`, where `atom` is an atom and `lot` a list of types which matches the requirements of the atom. We say that `Ty` *interprets* the `atom`. Going back to the previous examples:++```haskell+Ty V0 Int = Int+Ty V1 :@: (Maybe :$: V0) (Bool :&&: [] :&&: LoT0) = [Maybe Bool]+```++This bridge is used in the first of the pattern functors that `kind-generics` add to those from `GHC.Generics`. The pattern functor `F` is used to represent fields in a constructor, where the type is represented by an atom. Compare its definition with the `K1` type from `GHC.Generics`:++```haskell+newtype F (t :: Atom d (*)) (x :: LoT d) = F { unF :: Ty t x }+newtype K1 i (t :: *) = K1 { unK1 :: t }+```++At the term level there is almost no difference in the usage, except for the fact that fields are wrapped in the `F` constructor instead of `K1`.++```haskell+instance GenericK Tree (a :&&: LoT0) where+ type RepK Tree = (F (Tree :$: V0) :*: F (Tree :$: V0)) :+: (F V0)++ fromK (Branch l r) = L1 (F l :*: F r)+ fromK (Node x) = R1 (F x)+```++On the other hand, separating the atom from the list of types gives us the ability to interpret the same atom with different list of types. This is paramount to classes like `Functor`, in which the same type constructor is applied to different type variables.++## Functors for GADTS: `(:=>:)` and `E`++Generalised Algebraic Data Types, GADTs for short, extend the capabilities of Haskell data types. Once the extension is enabled, constructor gain the ability to constrain the set of allowed types, and to introduce existential types. Here is an extension of the previously-defined `Tree` type to include an annotation in every leaf, each of them with possibly a different type, and also require `Show` for the `a`s:++```haskell+data WeirdTree a where+ WeirdBranch :: WeirdTree a -> WeirdTree a -> WeirdTree a + WeirdLeaf :: Show a => t -> a -> WeirdTree a+```++The family of pattern functors `U1`, `F`, `(:+:)`, and `(:*:)` is not enough. Let us see what other things we use in the representation of `WeirdTree`:++```haskell+instance GenericK WeirdTree (a :&&: LoT0) where+ type RepK WeirdTree+ = F (WeirdTree :$: V0) :*: F (WeirdTree :$: V0)+ :+: E ((Show :$: V1) :=>: (F V0 :*: F V1))+```++Here the `(:=>:)` pattern functor plays the role of `=>` in the definition of the data type. It reuses the same notion of atoms from `F`, but requiring those atoms to give back a constraint instead of a ground type.++But wait a minute! You have just told me that the first type variable is represented by `V0`, and in the representation above `Show a` is transformed into `Show :$: V1`, what is going on? This change stems from `E`, which represents existential quantification. Whenever you go inside an `E`, you gain a new type variable in your list of types. This new variable is put *at the front* of the list of types, shifting all the other one position. In the example above, inside the `E` the atom `V0` points to `t`, and `V1` points to `a`. This approach implies that inside nested existentials the innermost variable corresponds to head of the list of types `V0`.++Unfortunately, at this point you need to write your own conversion functions if you use any of these extended features (pull requests implementing it in Template Haskell are more than welcome).++```haskell+instance GenericK WeirdTree (a :&&: LoT0) where+ type RepK WeirdTree = ...++ fromK (WeirdBranch l r) = L1 $ F l :*: F r+ fromK (WeirdLeaf a x) = R1 $ E $ C $ F a :*: F x++ toK ...+```++If you have ever done this work in `GHC.Generics`, there is not a big step. You just need to apply the `E` and `C` constructor every time there is an existential or constraint, respectively. However, since the additional information required by those types is implicitly added by the compiler, you do not need to write anything else.++## Implementing a generic operation with `kind-generics`++The last stop in our journey through `kind-generics` is being able to implement a generic operation. At this point we assume that the reader is comfortable with the definition of generic operations using `GHC.Generics`, so only the differences with that style are pointed out.++Take an operation like `Show`. Using `GHC.Generics` style, you create a type class whose instances are the corresponding pattern functors:++```haskell+class GShow (f :: * -> *) where+ gshow :: f x -> String++instance GShow U1 ...+instance Show t => GShow (K1 i t) ...+instance (GShow f, GShow g) => GShow (f :+: g) ...+instance (GShow f, GShow g) => GShow (f :*: g) ...+```++When using `kind-generics`, the type class needs to feature the separation between the head and its type arguments, in a similar way to `GenericK`. In this case, that means extending the class with a new parameter, and reworking the basic cases to include that argument.++```haskell+class GShow (f :: LoT k -> *) (x :: LoT k) where+ gshow :: f :@@: x -> String++instance GShow U1 x ...+instance (GShow f x, GShow g x) => GShow (f :+: g) x ...+instance (GShow f x, GShow g x) => GShow (f :*: g) x ...+```++Now we have the three new constructors. Let us start with `F atom`: when is it `Show`able? Whenever the interpretation of the atom, with the given list of types, satisfies the `Show` constraint. We can use the type family `Ty` to express this fact:++```haskell+instance (Show (Ty a x)) => GShow (F a) x where+ gshow (F x) = show x+```++In the case of existential constraints we do not need to enforce any additional constraints. However, we need to extend our list of types with a new one for the existential. We can do that using the `QuantifiedConstraints` extension introduced in GHC 8.6:++```haskell+{-# language QuantifiedConstraints #-}++instance (forall t. Show f (t :&&: x)) => GShow (E f) x where+ gshow (E x) = gshow x+```++The most interesting case is the one for constraints. If we have a constraint in a constructor, we know that by pattern matching on it we can use the constraint. In other words, we are allowed to assume that the constraint at the left-hand side of `(:=>:)` holds when trying to decide whether `GShow` does. This is again allowed by the `QuantifiedConstraints` extension:++```haskell+{-# language QuantifiedConstraints #-}++instance (Ty c x => GShow f x) => GShow (c :=>: f) x where+ gshow (C x) = gshow x+```++Note that sometimes we cannot implement a generic operation for every GADT. One example is generic equality (which you can find in the module `Generics.Kind.Derive.Eq`): when faced with two values of a constructor with an existential, we cannot move forward, since we have no way of knowing if the types enclosed by each value are the same or not.++## Conclusion and limitations++The `kind-generics` library extends the support for data type-generic programming from `GHC.Generics` to account for kinds different from `*` and `* -> *` and for GADTs. We have tried to reuse as much information as possible from what the compiler already gives us for free, in particular you can obtain a `GenericK` instance if you already have a `Generic` one.++Although we can now express a larger amount of types and operations, not *all* Haskell data types are expressible in this language. In particular, we cannot have *dependent* kinds, like in the following data type:++```haskell+data Proxy k (d :: k) = Proxy+```++because the kind of the second argument `d` refers to the first argument `k`.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ kind-generics.cabal view
@@ -0,0 +1,30 @@+cabal-version: >=1.10+name: kind-generics+version: 0.1.0.0+synopsis: Generic programming in GHC style for arbitrary kinds and GADTs.+description: This package provides functionality to extend the data type generic programming functionality in GHC to classes of arbitrary kind, and constructors featuring constraints and existentials, as usually gound in GADTs.+-- bug-reports:+license: BSD3+license-file: LICENSE+author: Alejandro Serrano+maintainer: trupill@gmail.com+-- copyright:+category: Data+build-type: Simple+extra-source-files: README.md++source-repository head+ type: git+ location: https://gitlab.com/trupill/kind-generics.git++library+ exposed-modules: Generics.Kind,+ Generics.Kind.Examples,+ Generics.Kind.Derive.Eq,+ Generics.Kind.Derive.Functor+ -- other-modules:+ -- other-extensions:+ build-depends: base >=4.12 && <5, kind-apply+ hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -Wall
+ src/Generics/Kind.hs view
@@ -0,0 +1,162 @@+{-# language DataKinds #-}+{-# language KindSignatures #-}+{-# language PolyKinds #-}+{-# language TypeFamilies #-}+{-# language GADTs #-}+{-# language ConstraintKinds #-}+{-# language TypeOperators #-}+{-# language StandaloneDeriving #-}+{-# language FlexibleContexts #-}+{-# language UndecidableInstances #-}+{-# language MultiParamTypeClasses #-}+{-# language FlexibleInstances #-}+{-# language ExistentialQuantification #-}+{-# language DefaultSignatures #-}+{-# language ScopedTypeVariables #-}+{-# language TypeApplications #-}+{-# language AllowAmbiguousTypes #-}+{-# language QuantifiedConstraints #-}+-- | Main module of @kind-generics@. Please refer to the @README@ file for documentation on how to use this package.+module Generics.Kind (+ module Data.PolyKinded+, module Data.PolyKinded.Atom+ -- * Generic representation types+, (:+:)(..), (:*:)(..), U1(..), M1(..)+, F(..), (:=>:)(..), E(..)+ -- * Generic type classes+, GenericK(..)+, GenericF, fromF, toF+, GenericN, fromN, toN+, GenericS, fromS, toS+ -- * Bridging with "GHC.Generics"+, Conv(..)+) where++import Data.PolyKinded+import Data.PolyKinded.Atom+import Data.Kind+import GHC.Generics.Extra hiding ((:=>:))+import qualified GHC.Generics.Extra as GG++-- | Fields: used to represent each of the (visible) arguments to a constructor.+-- Replaces the 'K1' type from "GHC.Generics". The type of the field is+-- represented by an 'Atom' from "Data.PolyKinded.Atom".+--+-- > instance GenericK [] (a :&&: LoT0) where+-- > type RepK [] = F V0 :*: F ([] :$: V0)+newtype F (t :: Atom d (*)) (x :: LoT d) = F { unF :: Ty t x }+deriving instance Show (Ty t x) => Show (F t x)++-- | Constraints: used to represent constraints in a constructor.+-- Replaces the '(:=>:)' type from "GHC.Generics.Extra".+--+-- > data Showable a = Show a => a -> X a+-- >+-- > instance GenericK Showable (a :&&: LoT0) where+-- > type RepK Showable = (Show :$: a) :=>: (F V0)+data (:=>:) (c :: Atom d Constraint) (f :: LoT d -> *) (x :: LoT d) where+ C :: Ty c x => f x -> (c :=>: f) x++-- | Existentials: a representation of the form @E f@ describes+-- a constructor whose inner type is represented by @f@, and where+-- the type variable at index 0, @V0@, is existentially quantified.+--+-- > data Exists where+-- > E :: t -> Exists+-- >+-- > instance GenericK Exists LoT0 where+-- > type RepK Exists = E (F V0)+data E (f :: LoT (k -> d) -> *) (x :: LoT d) where+ E :: forall (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d)+ . f (t ':&&: x) -> E f x++-- THE TYPE CLASS++-- | Representable types of any kind. The definition of an instance must+-- mention the type constructor along with a list of types of the corresponding+-- length. For example:+--+-- > instance GenericK Int LoT0+-- > instance GenericK [] (a :&&: LoT0)+-- > instance GenericK Either (a :&&: b :&&: LoT0)+class GenericK (f :: k) (x :: LoT k) where+ type RepK f :: LoT k -> *+ + -- | Convert the data type to its representation.+ fromK :: f :@@: x -> RepK f x+ default+ fromK :: (Generic (f :@@: x), Conv (Rep (f :@@: x)) (RepK f) x)+ => f :@@: x -> RepK f x+ fromK = toKindGenerics . from++ -- | Convert from a representation to its corresponding data type.+ toK :: RepK f x -> f :@@: x+ default+ toK :: (Generic (f :@@: x), Conv (Rep (f :@@: x)) (RepK f) x)+ => RepK f x -> f :@@: x+ toK = to . toGhcGenerics++type GenericF t f x = (GenericK f x, x ~ (SplitF t f), t ~ (f :@@: x))+fromF :: forall f t x. GenericF t f x => t -> RepK f x+fromF = fromK @_ @f+toF :: forall f t x. GenericF t f x => RepK f x -> t+toF = toK @_ @f++type GenericN n t f x = (GenericK f x, 'TyEnv f x ~ (SplitN n t), t ~ (f :@@: x))+fromN :: forall n t f x. GenericN n t f x => t -> RepK f x+fromN = fromK @_ @f+toN :: forall n t f x. GenericN n t f x => RepK f x -> t+toN = toK @_ @f++-- | @GenericS t f x@ states that the ground type @t@ is split by+-- default as the constructor @f@ and a list of types @x$, and that+-- a 'GenericK' instance exists for that constructor.+--+-- This constraint provides an external interface similar to that+-- provided by 'Generic' in "GHC.Generics".+type GenericS t f x = (Split t f x, GenericK f x)+fromS :: forall t f x. GenericS t f x => t -> RepK f x+fromS = fromF @f+toS :: forall t f x. GenericS t f x => RepK f x -> t+toS = toF @f++-- CONVERSION BETWEEN GHC.GENERICS AND KIND-GENERICS++-- | Bridges a representation of a data type using the combinators+-- in "GHC.Generics" with a representation using this module.+-- You are never expected to manipulate this type class directly,+-- it is part of the deriving mechanism for 'GenericK'.+class Conv (gg :: * -> *) (kg :: LoT d -> *) (tys :: LoT d) where+ toGhcGenerics :: kg tys -> gg a+ toKindGenerics :: gg a -> kg tys++instance Conv U1 U1 tys where+ toGhcGenerics U1 = U1+ toKindGenerics U1 = U1++instance (Conv f f' tys, Conv g g' tys) => Conv (f :+: g) (f' :+: g') tys where+ toGhcGenerics (L1 x) = L1 (toGhcGenerics x)+ toGhcGenerics (R1 x) = R1 (toGhcGenerics x)+ toKindGenerics (L1 x) = L1 (toKindGenerics x)+ toKindGenerics (R1 x) = R1 (toKindGenerics x)++instance (Conv f f' tys, Conv g g' tys) => Conv (f :*: g) (f' :*: g') tys where+ toGhcGenerics (x :*: y) = toGhcGenerics x :*: toGhcGenerics y+ toKindGenerics (x :*: y) = toKindGenerics x :*: toKindGenerics y++instance {-# OVERLAPPABLE #-} (Conv f f' tys) => Conv (M1 i c f) f' tys where+ toGhcGenerics x = M1 (toGhcGenerics x)+ toKindGenerics (M1 x) = toKindGenerics x++instance {-# OVERLAPS #-} (Conv f f' tys) => Conv (M1 i c f) (M1 i c f') tys where+ toGhcGenerics (M1 x) = M1 (toGhcGenerics x)+ toKindGenerics (M1 x) = M1 (toKindGenerics x)++instance (k ~ Ty t tys, Conv f f' tys)+ => Conv (k GG.:=>: f) (t :=>: f') tys where+ toGhcGenerics (C x) = SuchThat (toGhcGenerics x)+ toKindGenerics (SuchThat x) = C (toKindGenerics x)++instance (k ~ Ty t tys) => Conv (K1 p k) (F t) tys where+ toGhcGenerics (F x) = K1 x+ toKindGenerics (K1 x) = F x
+ src/Generics/Kind/Derive/Eq.hs view
@@ -0,0 +1,48 @@+{-# language DataKinds #-}+{-# language PolyKinds #-}+{-# language KindSignatures #-}+{-# language MultiParamTypeClasses #-}+{-# language QuantifiedConstraints #-}+{-# language TypeOperators #-}+{-# language FlexibleInstances #-}+{-# language FlexibleContexts #-}+{-# language UndecidableInstances #-}+{-# language AllowAmbiguousTypes #-}+{-# language ScopedTypeVariables #-}+{-# language TypeFamilies #-}+{-# language TypeApplications #-}+module Generics.Kind.Derive.Eq where++import Generics.Kind++geq' :: forall t f x. (GenericS t f x, GEq (RepK f) x)+ => t -> t -> Bool+geq' x y = geq (fromS x) (fromS y)++class GEq (f :: LoT k -> *) (tys :: LoT k) where+ geq :: f tys -> f tys -> Bool++instance GEq U1 tys where+ geq U1 U1 = True++instance (GEq f tys) => GEq (M1 i c f) tys where+ geq (M1 x) (M1 y) = geq x y++instance (GEq f tys, GEq g tys) => GEq (f :+: g) tys where+ geq (L1 x) (L1 y) = geq x y+ geq (R1 x) (R1 y) = geq x y+ geq _ _ = False++instance (GEq f tys, GEq g tys) => GEq (f :*: g) tys where+ geq (x1 :*: x2) (y1 :*: y2) = geq x1 y1 && geq x2 y2++instance (Eq (Ty t tys)) => GEq (F t) tys where+ geq (F x) (F y) = x == y++instance (Ty c tys => GEq f tys) => GEq (c :=>: f) tys where+ geq (C x) (C y) = geq x y++{- We cannot check whether the two existentials have the same type+instance (forall t. GEq f (t :&&: tys)) => GEq (E f) tys where+ geq (E x) (E y) = geq x y+-}
+ src/Generics/Kind/Derive/Functor.hs view
@@ -0,0 +1,105 @@+{-# language DataKinds #-}+{-# language PolyKinds #-}+{-# language GADTs #-}+{-# language RankNTypes #-}+{-# language TypeOperators #-}+{-# language MultiParamTypeClasses #-}+{-# language FlexibleInstances #-}+{-# language FlexibleContexts #-}+{-# language QuantifiedConstraints #-}+{-# language UndecidableInstances #-}+{-# language ScopedTypeVariables #-}+{-# language FunctionalDependencies #-}+{-# language TypeApplications #-}+{-# language DefaultSignatures #-}+{-# language AllowAmbiguousTypes #-}+{-# language TypeFamilies #-}+module Generics.Kind.Derive.Functor where++import Data.PolyKinded.Functor+import Data.Proxy++import Generics.Kind++kfmapDefault :: forall (f :: k) v as bs. (GenericK f as, GenericK f bs, GFunctor (RepK f) v as bs)+ => Mappings v as bs -> f :@@: as -> f :@@: bs+kfmapDefault v = toK @k @f @bs . gfmap v . fromK @k @f @as++fmapDefault :: forall (f :: * -> *) a b.+ (GenericK f (a ':&&: 'LoT0), GenericK f (b ':&&: 'LoT0),+ GFunctor (RepK f) '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0))+ => (a -> b) -> f a -> f b+fmapDefault f = kfmapDefault (f :^: M0 :: Mappings '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0))++class GFunctor (f :: LoT k -> *) (v :: Variances) (as :: LoT k) (bs :: LoT k) where+ gfmap :: Mappings v as bs -> f as -> f bs++instance GFunctor U1 v as bs where+ gfmap _ U1 = U1++instance GFunctor f v as bs => GFunctor (M1 i c f) v as bs where+ gfmap v (M1 x) = M1 (gfmap v x)++instance (GFunctor f v as bs, GFunctor g v as bs)+ => GFunctor (f :+: g) v as bs where+ gfmap v (L1 x) = L1 (gfmap v x)+ gfmap v (R1 x) = R1 (gfmap v x)++instance (GFunctor f v as bs, GFunctor g v as bs)+ => GFunctor (f :*: g) v as bs where+ gfmap v (x :*: y) = gfmap v x :*: gfmap v y++instance (Ty c as => GFunctor f v as bs, {- Ty c as => -} Ty c bs)+ => GFunctor (c :=>: f) v as bs where+ gfmap v (C x) = C (gfmap v x)++instance forall f v as bs.+ (forall (t :: *). GFunctor f ('Co ': v) (t ':&&: as) (t ':&&: bs))+ => GFunctor (E f) v as bs where+ gfmap v (E (x :: f (t ':&&: x))) = E (gfmap ((id :^: v) :: Mappings ('Co ': v) (t ':&&: as) (t ':&&: bs)) x)++class GFunctorArg (t :: Atom d (*))+ (v :: Variances) (intended :: Variance)+ (as :: LoT d) (bs :: LoT d) where+ gfmapf :: Proxy t -> Proxy intended+ -> Mappings v as bs+ -> Mapping intended (Ty t as) (Ty t bs)++instance forall t v as bs. GFunctorArg t v 'Co as bs+ => GFunctor (F t) v as bs where+ gfmap v (F x) = F (gfmapf (Proxy @t) (Proxy @'Co) v x)++instance GFunctorArg ('Kon t) v 'Co as bs where+ gfmapf _ _ _ = id+instance GFunctorArg ('Kon t) v 'Contra as bs where+ gfmapf _ _ _ = id++instance GFunctorArg ('Var 'VZ) (r ': v) r (a ':&&: as) (b ':&&: bs) where+ gfmapf _ _ (f :^: _) = f++instance forall vr pre v intended a as b bs.+ GFunctorArg ('Var vr) v intended as bs+ => GFunctorArg ('Var ('VS vr)) (pre ': v) intended (a ':&&: as) (b ':&&: bs) where+ gfmapf _ _ (_ :^: rest) = gfmapf (Proxy @('Var vr)) (Proxy @intended) rest++instance forall f x v v1 as bs.+ (KFunctor f '[v1] (Ty x as ':&&: 'LoT0) (Ty x bs ':&&: 'LoT0),+ GFunctorArg x v v1 as bs)+ => GFunctorArg (f :$: x) v 'Co as bs where+ gfmapf _ _ v = kfmap (gfmapf (Proxy @x) (Proxy @v1) v :^: M0)++instance forall f x y v v1 v2 as bs.+ (KFunctor f '[v1, v2] (Ty x as ':&&: Ty y as ':&&: 'LoT0) (Ty x bs ':&&: Ty y bs ':&&: 'LoT0),+ GFunctorArg x v v1 as bs, GFunctorArg y v v2 as bs)+ => GFunctorArg (f :$: x ':@: y) v 'Co as bs where+ gfmapf _ _ v = kfmap (gfmapf (Proxy @x) (Proxy @v1) v :^:+ gfmapf (Proxy @y) (Proxy @v2) v :^: M0)++instance forall f x y z v v1 v2 v3 as bs.+ (KFunctor f '[v1, v2, v3] (Ty x as ':&&: Ty y as ':&&: Ty z as ':&&: 'LoT0)+ (Ty x bs ':&&: Ty y bs ':&&: Ty z bs ':&&: 'LoT0),+ GFunctorArg x v v1 as bs, GFunctorArg y v v2 as bs, GFunctorArg z v v3 as bs)+ => GFunctorArg (f :$: x ':@: y ':@: z) v 'Co as bs where+ gfmapf _ _ v = kfmap (gfmapf (Proxy @x) (Proxy @v1) v :^:+ gfmapf (Proxy @y) (Proxy @v2) v :^:+ gfmapf (Proxy @z) (Proxy @v3) v :^: M0)
+ src/Generics/Kind/Examples.hs view
@@ -0,0 +1,64 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# language TypeOperators #-}+{-# language TypeFamilies #-}+{-# language DataKinds #-}+{-# language MultiParamTypeClasses #-}+{-# language FlexibleInstances #-}+{-# language GADTs #-}+{-# language DeriveGeneric #-}+module Generics.Kind.Examples where++import Data.PolyKinded.Functor+import GHC.Generics (Generic)++import Generics.Kind+import Generics.Kind.Derive.Eq+import Generics.Kind.Derive.Functor++-- Obtained from Generic++instance Split (Maybe a) Maybe (a ':&&: 'LoT0)+instance GenericK Maybe (a ':&&: 'LoT0) where+ type RepK Maybe = U1 :+: F V0++instance KFunctor Maybe '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where+ kfmap = kfmapDefault++-- From the docs++data Tree a = Branch (Tree a) (Tree a) | Leaf a+ deriving Generic++instance Split (Tree a) Tree (a ':&&: 'LoT0)+instance GenericK Tree (a ':&&: 'LoT0) where+ type RepK Tree = F (Tree :$: V0) :*: F (Tree :$: V0) :+: F V0++instance Eq a => Eq (Tree a) where+ (==) = geq'++instance KFunctor Tree '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where+ kfmap = kfmapDefault++instance Functor Tree where+ fmap = fmapDefault++-- Hand-written instance++data WeirdTree a where+ WeirdBranch :: WeirdTree a -> WeirdTree a -> WeirdTree a + WeirdLeaf :: Show a => t -> a -> WeirdTree a++instance Split (WeirdTree a) WeirdTree (a ':&&: 'LoT0)+instance GenericK WeirdTree (a ':&&: 'LoT0) where+ type RepK WeirdTree+ = F (WeirdTree :$: V0) :*: F (WeirdTree :$: V0)+ :+: E ((Show :$: V1) :=>: (F V0 :*: F V1))++ fromK (WeirdBranch l r) = L1 $ F l :*: F r+ fromK (WeirdLeaf a x) = R1 $ E $ C $ F a :*: F x++ toK (L1 (F l :*: F r)) = WeirdBranch l r+ toK (R1 (E (C (F a :*: F x)))) = WeirdLeaf a x++instance Show b => KFunctor WeirdTree '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0) where+ kfmap = kfmapDefault