on 137ebed help sign in
93 lines 2.5 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language DataKinds #-}
3{-# language EmptyCase #-}
4{-# language FlexibleInstances #-}
5{-# language LambdaCase #-}
6{-# language MultiParamTypeClasses #-}
7{-# language RankNTypes #-}
8{-# language ScopedTypeVariables #-}
9{-# language StandaloneKindSignatures #-}
10{-# language TypeApplications #-}
11{-# language TypeFamilies #-}
12{-# language TypeOperators #-}
13{-# language UndecidableInstances #-}
15module Rel8.Generic.Map
16 ( GMap, GMappable (gmap, gunmap)
17 )
18where
20-- base
21import Data.Kind ( Constraint, Type )
22import GHC.Generics
23 ( (:+:)( L1, R1 ), (:*:)( (:*:) ), K1( K1 ), M1( M1 ), U1( U1 ), V1
24 )
25import Prelude ()
27-- rel8
28import Rel8.FCF ( Eval, Exp )
31type GMap :: (Type -> Exp Type) -> (Type -> Type) -> Type -> Type
32type family GMap f rep where
33 GMap f (M1 i c rep) = M1 i c (GMap f rep)
34 GMap _ V1 = V1
35 GMap f (rep1 :+: rep2) = GMap f rep1 :+: GMap f rep2
36 GMap _ U1 = U1
37 GMap f (rep1 :*: rep2) = GMap f rep1 :*: GMap f rep2
38 GMap f (K1 i a) = K1 i (Eval (f a))
41type GMappable :: (Type -> Exp Constraint) -> (Type -> Type) -> Constraint
42class GMappable constraint rep where
43 gmap :: ()
44 => proxy f
45 -> (forall a. Eval (constraint a) => a -> Eval (f a))
46 -> rep x
47 -> GMap f rep x
49 gunmap :: ()
50 => proxy f
51 -> (forall a. Eval (constraint a) => Eval (f a) -> a)
52 -> GMap f rep x
53 -> rep x
56instance GMappable constraint rep => GMappable constraint (M1 i c rep) where
57 gmap proxy f (M1 a) = M1 (gmap @constraint proxy f a)
58 gunmap proxy f (M1 a) = M1 (gunmap @constraint proxy f a)
61instance GMappable constraint V1 where
62 gmap _ _ = \case
63 gunmap _ _ = \case
66instance (GMappable constraint rep1, GMappable constraint rep2) =>
67 GMappable constraint (rep1 :+: rep2)
68 where
69 gmap proxy f = \case
70 L1 a -> L1 (gmap @constraint proxy f a)
71 R1 a -> R1 (gmap @constraint proxy f a)
72 gunmap proxy f = \case
73 L1 a -> L1 (gunmap @constraint proxy f a)
74 R1 a -> R1 (gunmap @constraint proxy f a)
77instance GMappable constraint U1 where
78 gmap _ _ U1 = U1
79 gunmap _ _ U1 = U1
82instance (GMappable constraint rep1, GMappable constraint rep2) =>
83 GMappable constraint (rep1 :*: rep2)
84 where
85 gmap proxy f (a :*: b) =
86 gmap @constraint proxy f a :*: gmap @constraint proxy f b
87 gunmap proxy f (a :*: b) =
88 gunmap @constraint proxy f a :*: gunmap @constraint proxy f b
91instance Eval (constraint a) => GMappable constraint (K1 i a) where
92 gmap _ f (K1 a) = K1 (f a)
93 gunmap _ f (K1 a) = K1 (f a)