General.v: add boolean and/or functions
[coq-hetmet.git] / examples / IsomorphismForCodeTypes.hs
1 {-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds #-}
2 module IsomorphismForCodeTypes
3 where
4
5 --------------------------------------------------------------------------------
6 -- Taha-Sheard "isomorphism for code types"
7
8 back  :: forall a b c. (<[b]>@a -> <[c]>@a) -> <[ b->c ]>@a
9 back  = \f -> <[ \x -> ~~(f <[x]>) ]>
10
11 forth :: forall a b c. <[b->c]>@a -> (<[b]>@a -> <[c]>@a)
12 forth = \f -> \x -> <[ ~~f ~~x ]>