on da76712 help sign in
rel8/src/Rel8/Schema/HTable/MapTable.hs
99 lines 2.7 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language BlockArguments #-}
3{-# language ConstraintKinds #-}
4{-# language DataKinds #-}
5{-# language FlexibleInstances #-}
6{-# language GADTs #-}
7{-# language InstanceSigs #-}
8{-# language MultiParamTypeClasses #-}
9{-# language RankNTypes #-}
10{-# language ScopedTypeVariables #-}
11{-# language StandaloneKindSignatures #-}
12{-# language TypeApplications #-}
13{-# language TypeFamilies #-}
14{-# language UndecidableInstances #-}
15{-# language UndecidableSuperClasses #-}
17module Rel8.Schema.HTable.MapTable
18 ( HMapTable(..)
19 , MapSpec(..)
20 , Precompose(..)
21 , HMapTableField(..)
22 , hproject
23 )
24where
26-- base
27import Data.Kind ( Constraint, Type )
28import Prelude
30-- rel8
31import Rel8.FCF ( Exp, Eval )
32import Rel8.Schema.HTable
33 ( HTable, HConstrainTable, HField
34 , hfield, htabulate, htraverse, hdicts, hspecs
35 )
36import Rel8.Schema.Spec ( Spec )
37import qualified Rel8.Schema.Kind as K
38import Rel8.Schema.Dict ( Dict( Dict ) )
41type HMapTable :: (Type -> Exp Type) -> K.HTable -> K.HTable
42newtype HMapTable f t context = HMapTable
43 { unHMapTable :: t (Precompose f context)
44 }
47type Precompose :: (Type -> Exp Type) -> K.Context -> K.Context
48newtype Precompose f g x = Precompose
49 { precomposed :: g (Eval (f x))
50 }
53type HMapTableField :: (Type -> Exp Type) -> K.HTable -> K.Context
54data HMapTableField f t x where
55 HMapTableField :: HField t a -> HMapTableField f t (Eval (f a))
58instance (HTable t, MapSpec f) => HTable (HMapTable f t) where
59 type HField (HMapTable f t) =
60 HMapTableField f t
62 type HConstrainTable (HMapTable f t) c =
63 HConstrainTable t (ComposeConstraint f c)
65 hfield (HMapTable x) (HMapTableField i) =
66 precomposed (hfield x i)
68 htabulate f =
69 HMapTable $ htabulate (Precompose . f . HMapTableField)
71 htraverse f (HMapTable x) =
72 HMapTable <$> htraverse (fmap Precompose . f . precomposed) x
73 {-# INLINABLE htraverse #-}
75 hdicts :: forall c. HConstrainTable (HMapTable f t) c => HMapTable f t (Dict c)
76 hdicts =
77 htabulate \(HMapTableField j) ->
78 case hfield (hdicts @_ @(ComposeConstraint f c)) j of
79 Dict -> Dict
81 hspecs =
82 HMapTable $ htabulate $ Precompose . mapInfo @f . hfield hspecs
83 {-# INLINABLE hspecs #-}
86type MapSpec :: (Type -> Exp Type) -> Constraint
87class MapSpec f where
88 mapInfo :: Spec x -> Spec (Eval (f x))
91type ComposeConstraint :: (Type -> Exp Type) -> (Type -> Constraint) -> Type -> Constraint
92class c (Eval (f a)) => ComposeConstraint f c a
93instance c (Eval (f a)) => ComposeConstraint f c a
96hproject :: ()
97 => (forall ctx. t ctx -> t' ctx)
98 -> HMapTable f t context -> HMapTable f t' context
99hproject f (HMapTable a) = HMapTable (f a)