Skip to content

Instantly share code, notes, and snippets.

@edwinb
Created May 18, 2014 18:28
Show Gist options
  • Save edwinb/8c51062165bf180eaa8a to your computer and use it in GitHub Desktop.
Save edwinb/8c51062165bf180eaa8a to your computer and use it in GitHub Desktop.
Lazy hack
data Strategy : Type where
MkStrategy : (t : Type -> Type) ->
(delay : (a : Type) -> a -> t a) ->
(force : (a : Type) -> t a -> a) ->
Strategy
strategy : Strategy -> Type -> Type
strategy (MkStrategy t delay force) = t
delay : {s : Strategy} -> {a : Type} -> a -> strategy s a
delay {s = (MkStrategy t d f)} = d _
force : {s : Strategy} -> {a : Type} -> strategy s a -> a
force {s = (MkStrategy t d f)} = f _
AsLazy : Strategy
AsLazy = MkStrategy Lazy (\x => Delay) (\x => Force)
AsStrict : Strategy
AsStrict = MkStrategy id (\x => id) (\x => id)
data SList : Strategy -> Type -> Type where
Nil : SList s a
(::) : a -> strategy s (SList s a) -> SList s a
toList : SList s a -> List a
toList [] = []
toList (x :: xs) = x :: Main.toList (force xs)
take : Nat -> SList s a -> SList s a
take Z x = []
take (S k) [] = []
take (S k) (x :: xs) = x :: delay (Main.take k (force xs))
instance Show a => Show (SList s a) where
show x = show (Main.toList x)
ones : SList AsLazy Nat
ones = 1 :: ones
main : IO ()
main = print (take 10 ones)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment