Lazy hack

gistfile1.idr

  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)