loopAdmStream-Nat.ma

-- 2010-05-11

data Nat : Set
{ zero : Nat
; succ : Nat -> Nat
}

sized codata Stream (+ A : Set) : Size -> Set
{ cons : [i : Size] -> (head : A) -> (tail : Stream A i) -> Stream A ($ i)
}
fields head, tail

fun guard : [j : Size] -> (Stream Nat ($ j) -> Stream Nat #)
                       -> (Stream Nat j     -> Stream Nat #)
{ guard j g xs = g (cons j zero xs)
}

-- the type of f is not admissible
cofun f : [i : Size] -> (Stream Nat i -> Stream Nat #) -> Stream Nat i
{ f ($ j) g = guard j g (f j (guard j g))
}

-- LOOP!
eval let loop : Nat = head # (f # (tail #))

{-
-- the type of f is not admissible
cofun f : (Stream Nat # -> Stream Nat #) ->
  [i : Size] -> (Stream Nat i -> Stream Nat #) -> Stream Nat i
{ f h ($ j) g = h (g (cons j zero
    (f (\ x -> h (h x))
       j
       (\ x -> g (cons j zero x)))))
}

-}