The Coq mailing list

[Andrei Popescu <uuomul AT yahoo.com>]

Hi Andreas, 

Of course, sized types are an elegant and powerful solution. However, the 
parametricity-based alternative has the advantage that it needs no size 
annotations (and indeed, no annotations at all). On the downside, it is less 
expressive and does require discharging a parametricity goal, which can 
typically be done automatically using a standard parametricity prover though. 

Here is the Isabelle version of "flatten", using a sugar notation that is not 
yet available, but will hopefully be there in the next release:

codatatype 'a stream = Cons (head: 'a) (tail: "'a stream") (infixr "##" 65)

corec (well_behaved) prepend : 'a list => 'a stream => 'a stream
where 
  prepend as s = 
    (case as of [] => s
               |a # as => a ## prepend as s
    )
well_behavedness by parametricity_prover

(* at this point, prepend has been registered as well-behaved, hence it can 
participate in call contexts 
  for future corecursively defined functions *) 

corec flatten : ('a * 'a list) stream => 'a stream
where 
  flatten s = fst (head s) ## prepend (snd (head s)) (flatten (tail s))


All the best, 
  Andrei 


On Monday, August 25, 2014 8:23 PM, Andreas Abel 
<andreas.abel AT ifi.lmu.de>
 wrote:


Tracking guardedness in the type system does the job, this is your code 
in Agda:

{-# OPTIONS --copatterns #-}

open import Data.List
open import Data.Product renaming (proj₁ to fst; proj₂ to snd)
open import Size

record Stream (i : Size) (A : Set) : Set where
   coinductive
   constructor _∷_
   field
     head : A
     tail : ∀{j : Size< i} → Stream j A
open Stream

prepend : ∀{i A} → List A → Stream i A → Stream i A
prepend []       s = s
prepend (a ∷ as) s = a ∷ prepend as s

flatten : ∀{i
A} → Stream i (A × List A) → Stream i A
head (flatten s) = fst (head s)
tail (flatten s) = prepend (snd (head s)) (flatten (tail s))



On 22.08.2014 12:01, Andrei Popescu wrote:
> Greetings,
>
> I would like to advocate an approach for obtaining flexible corecursive
> principles in a light-weight fashion, without the need to modify the
> definitions or add any type annotations. The only overhead is the
> requirement to track parametricity.
>
> In short, many operations can be recorded as well-behaved (i.e., OK to
> appear in the corecursive call context along with constructors), after
> checking that their defining equation (i.e.,
technically, the structural
> operation of its defining coalgebra) has a parametric component. For
> example, if defined with CoFixpoint instead of Fixpoint, Jason's
> "stream_prepend_list" is well-behaved whereas the stream "tail" is not.
>
> The following paper describes the approach starting with simple
> examples, also covering mixed recursion-corecursion:
>
> http://www4.in.tum.de/~popescua/pdf/fouco.pdf
>
> My colleagues and I have implemented a prototype of this approach in
> Isabelle -- it is immediately applicable to the simple-type fragment of
> Coq. While not being an expert in Coq or dependent types, I believe that
> it can be extended to cope with dependent types as well, thanks to
> Bernardy's work on PTSparametricity and its follow-up implementation in
> Coq (http://www.lix.polytechnique.fr/%7Ekeller/Recherche/coqparam.html).
>
> At its core, this notion of safely enriching corecursion incrementally
> is not new, and has been advocated by category theorists for years.
> Unfortunately, it has not made it (yet) into mainstream theorem proving.
>
> All the best,
>    Andrei
>
>
>
>
> On Wednesday, August 20, 2014 6:32 PM, Jason Gross
> <jasongross9 AT gmail.com>
>  wrote:
>
>
>
> Hi,
> Why does Coq not notice that the following definition is manifestly
> productive?
>
> Require Import Coq.Lists.Streams.
>
> Fixpoint stream_prepend_list {T} (ls : list T) (rest : Stream T) :
> Stream T :=
>    match ls with
>      | nil => rest
>      | cons x xs => Cons x (stream_prepend_list xs rest)
>    end.
>
> CoFixpoint flatten_stream {T} (s : Stream (T * list T)) : Stream T :=
>    match s with
>      | Cons x xs => Cons (fst x) (stream_prepend_list (snd x)
> (flatten_stream xs))
>    end.
> (* Error:
> Recursive definition of flatten_stream is ill-formed.
> In environment
> flatten_stream : forall T : Type, Stream (T * list T) -> Stream T
> T : Type
> s : Stream (T * list T)
> x : T * list T
> xs : Stream (T * list T)
> Sub-expression "stream_prepend_list (snd x) (flatten_stream T xs)" not in
> guarded form (should be a constructor, an abstraction, a match, a cofix or a
> recursive call).
> Recursive definition is:
> "fun (T : Type) (s : Stream (T * list T)) =>
>   match s with
>   | Cons x xs =>
>       Cons (fst x) (stream_prepend_list (snd x) (flatten_stream T xs))
>   end". *)
>
>
> It seems that Coq doesn't want me to put anything between the recursive
> call and the constructor, but it's syntactically obvious that my
> definition is productive...
>
> -Jason


-- 
Andreas Abel  <><      Du bistdergeliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel AT gu.se
http://www2.tcs.ifi.lmu.de/~abel/