Skip to content

Instantly share code, notes, and snippets.

Created August 19, 2016 23:56
Show Gist options
  • Save anonymous/57262e4e1009e658b97e8986a2d03d40 to your computer and use it in GitHub Desktop.
Save anonymous/57262e4e1009e658b97e8986a2d03d40 to your computer and use it in GitHub Desktop.
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
module Test where
data D :: * -> * -> * where
Refl :: D a a
data T :: * -> * where
Nil :: T a
Cons :: (D a e) -> (e -> a) -> T a
newtype CpsT a = CpsT
{ runCpsT :: forall r .
r -> -- Nil
(forall e . D a e -> (e -> a) -> r) -> -- Cons
r }
uncps :: CpsT a -> T a
uncps p = runCpsT p Nil Cons
main = pure () :: IO ()
type (_, _) d =
Refl : ('a, 'a) d
type 'a t =
| Nil
| Cons : ('a, 'e) d * ('e -> 'a) -> 'a t
type 'a cps_t =
< get : 'r .
'r -> (* Nil *)
< get : 'e . ('a, 'e) d -> ('e -> 'a) -> 'r > -> (* Cons *)
'r >
(* Error: The universal variable 'e would escape its scope *)
let uncps : type a . a cps_t -> a t =
fun p -> p # get Nil (object method get d f = Cons (d, f) end)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment