git.iko.soy/rel8
on be54907 help sign in
rel8/src/Rel8/Generic/Coherence.hs
79 lines 2.3 kB history raw
1{-# language AllowAmbiguousTypes #-}
2{-# language DataKinds #-}
3{-# language FlexibleInstances #-}
4{-# language MultiParamTypeClasses #-}
5{-# language PolyKinds #-}
6{-# language RankNTypes #-}
7{-# language ScopedTypeVariables #-}
8{-# language StandaloneKindSignatures #-}
9{-# language TypeApplications #-}
10{-# language TypeFamilies #-}
11{-# language TypeOperators #-}
12{-# language UndecidableInstances #-}
14module Rel8.Generic.Coherence
15 ( GCoherent
16 , gcoherence
17 , gcongruence
18 )
19where
21-- base
22import Control.Category ( id )
23import Data.Kind ( Constraint, Type )
24import Data.Proxy ( Proxy( Proxy ) )
25import Data.Type.Equality ( (:~:), apply )
26import GHC.Generics ( (:*:), K1, M1, Meta( MetaSel ), C, D, S )
27import Prelude hiding ( id )
29-- rel8
30import Rel8.FCF ( Eval, Exp )
31import Rel8.Generic.Map ( GMap )
32import Rel8.Generic.Table.Record ( GColumns, GContext )
35type GCoherent :: (Type -> Exp Constraint) -> (Type -> Type) -> Constraint
36class GCoherent _Table rep where
37 gcoherence :: ()
38 => proxy _Context
39 -> proxy' f
40 -> (forall a proxy_. Eval (_Table a)
41 => proxy_ a -> Eval (_Context (Eval (f a))) :~: context)
42 -> GContext _Context (GMap f rep) :~: context
44 gcongruence :: ()
45 => proxy _Columns
46 -> proxy' f
47 -> (forall a proxy_. Eval (_Table a)
48 => proxy_ a -> Eval (_Columns a) :~: Eval (_Columns (Eval (f a))))
49 -> GColumns _Columns rep :~: GColumns _Columns (GMap f rep)
52instance GCoherent _Table rep => GCoherent _Table (M1 D c rep) where
53 gcoherence = gcoherence @_Table @rep
54 gcongruence = gcongruence @_Table @rep
57instance GCoherent _Table rep => GCoherent _Table (M1 C c rep) where
58 gcoherence = gcoherence @_Table @rep
59 gcongruence = gcongruence @_Table @rep
62instance (GCoherent _Table rep1, GCoherent _Table rep2) =>
63 GCoherent _Table (rep1 :*: rep2)
64 where
65 gcoherence = gcoherence @_Table @rep1
66 gcongruence _Columns f proof = id `apply`
67 gcongruence @_Table @rep1 _Columns f proof `apply`
68 gcongruence @_Table @rep2 _Columns f proof
71instance
72 ( Eval (_Table a)
73 , meta ~ 'MetaSel ('Just _l) _su _ss _ds
74 , k1 ~ K1 i a
75 )
76 => GCoherent _Table (M1 S meta k1)
77 where
78 gcoherence _ _ proof = proof (Proxy @a)
79 gcongruence _ _ proof = id `apply` proof (Proxy @a)