Skip to content

Instantly share code, notes, and snippets.

@jonsterling
Created October 13, 2012 22:46
Show Gist options
  • Save jonsterling/3886482 to your computer and use it in GitHub Desktop.
Save jonsterling/3886482 to your computer and use it in GitHub Desktop.
Idea for codata syntax in Haskell
-- Inspired by http://www2.tcs.ifi.lmu.de/~abel/popl13.pdf
[codata|
codata Stream a where
head :: Stream a -> a
tail :: Stream a -> Stream a
|]
fib :: Stream Nat
[copattern|
head fib = Z
head (tail fib) = S Z
tail (tail fib) = zipWith plus fib (tail fib)
|]
-- should translate roughly into:
data StreamOut t where
Head :: StreamOut (Stream a -> a)
Tail :: StreamOut (Stream a -> Stream a)
-- `Coinductive ds` denotes a set of evaluation rules for a data type
-- defined by its destructors `ds`.
newtype Coinductive ds a =
Coinduction { run :: forall r. ds (Coinductive ds a -> r) -> r }
type Stream = Coinductive StreamOut
head xs = run xs Head
tail xs = run xs Tail
fib :: Stream Nat
fib = Coinduction $ \case
Head -> Z
Tail -> Coinduction $ \case
Head -> S Z
Tail -> zipWith plus fib (tail fib)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment