blob: c76dfb962ede43b9a1105aedf009e71c34d2c9e7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
-- Based on https://github.com/idris-lang/Idris-dev/blob/v0.9.10/libs/effects/Effects.idr
{-# LANGUAGE DataKinds, PolyKinds, ScopedTypeVariables, TypeOperators,
TypeApplications, GADTs, TypeFamilies, AllowAmbiguousTypes #-}
module T12442 where
import Data.Kind
data family Sing (a :: k)
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family (a :: k1 ~> k2) @@ (b :: k1) :: k2
data TyCon1 :: (Type -> Type) -> (Type ~> Type)
type instance (TyCon1 t) @@ x = t x
data TyCon2 :: (Type -> Type -> Type) -> (Type ~> Type ~> Type)
type instance (TyCon2 t) @@ x = (TyCon1 (t x))
data TyCon3 :: (Type -> Type -> Type -> Type) -> (Type ~> Type ~> Type ~> Type)
type instance (TyCon3 t) @@ x = (TyCon2 (t x))
type Effect = Type ~> Type ~> Type ~> Type
data EFFECT :: Type where
MkEff :: Type -> Effect -> EFFECT
data EffElem :: (Type ~> Type ~> Type ~> Type) -> Type -> [EFFECT] -> Type where
Here :: EffElem x a (MkEff a x ': xs)
data instance Sing (elem :: EffElem x a xs) where
SHere :: Sing Here
type family UpdateResTy b t (xs :: [EFFECT]) (elem :: EffElem e a xs)
(thing :: e @@ a @@ b @@ t) :: [EFFECT] where
UpdateResTy b _ (MkEff a e ': xs) Here n = MkEff b e ': xs
data EffM :: (Type ~> Type) -> [EFFECT] -> [EFFECT] -> Type -> Type
effect :: forall e a b t xs prf eff m.
Sing (prf :: EffElem e a xs)
-> Sing (eff :: e @@ a @@ b @@ t)
-> EffM m xs (UpdateResTy b t xs prf eff) t
effect = undefined
data State :: Type -> Type -> Type -> Type where
Get :: State a a a
data instance Sing (e :: State a b c) where
SGet :: Sing Get
type STATE t = MkEff t (TyCon3 State)
get_ :: forall m x. EffM m '[STATE x] '[STATE x] x
get_ = effect @(TyCon3 State) SHere SGet
|
