Skip to content

Instantly share code, notes, and snippets.

@jroesch

jroesch/Example.hs

Created May 29, 2014 02:52
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save jroesch/0fc24965995257347d29 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save jroesch/0fc24965995257347d29 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Example.hs
{-# LANGUAGE RankNTypes #-}
data Result i r = Fail String
| Done i r
data ExType i a = ExType { extract :: forall r. a -> Result i r }
fail :: String -> ExType i a
fail s = ExType (\x -> Fail "bleh")
Raw
Example.idr
module Example
data Result i r = Fail String
| Done i r
data ExType i a = MkExType (r : Type ** a -> Result i r)
fail : String -> ExType i a
fail s = MkExType (_ ** (\x => Fail "bleh"))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment