X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FIsomorphismForCodeTypes.hs;fp=examples%2FIsomorphismForCodeTypes.hs;h=6e245d7f9fa2bb50954b9bf5dcd8a0b990ebe74f;hp=0000000000000000000000000000000000000000;hb=caa7ad74b99b34abc5181553e66423da6bdfee26;hpb=e3e2ce9cb83acdd8191049b4e9bd3d4fcf6a4db4

diff --git a/examples/IsomorphismForCodeTypes.hs b/examples/IsomorphismForCodeTypes.hs
new file mode 100644
index 0000000..6e245d7
--- /dev/null
+++ b/examples/IsomorphismForCodeTypes.hs
@@ -0,0 +1,12 @@
+{-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds #-}
+module IsomorphismForCodeTypes
+where
+
+--------------------------------------------------------------------------------
+-- Taha-Sheard "isomorphism for code types"
+
+back  :: forall a b c. (<[b]>@a -> <[c]>@a) -> <[ b->c ]>@a
+back  = \f -> <[ \x -> ~~(f <[x]>) ]>
+
+forth :: forall a b c. <[b->c]>@a -> (<[b]>@a -> <[c]>@a)
+forth = \f -> \x -> <[ ~~f ~~x ]>