[Caml-list] recursive records

[Caml-list] recursive records

[Brigitte Pientka]

I am playing around with using recursive records to define observations about
streams simulating essentially the ideas described in "Copatterns:Programming infinite structures by observations" presented at POPL'13.

type 'a susp = Susp of (unit -> 'a)

type 'a str = {hd: 'a  ; tl : ('a str) susp}

let rec ones = {hd = 1 ; tl = Susp (fun () -> ones)}

This works fine and many examples can be elegantly written this way.  However,
when I define the stream ones via the function delay, OCaml fails.

  let delay f = Susp f

  let rec ones = {hd = 1 ; tl = delay (fun () -> ones)};;
Characters 15-53:
   let rec ones = {hd = 1 ; tl = delay (fun () -> ones)};;
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This kind of expression is not allowed as right-hand side of `let rec'

Could someone explain why this fails?

Thanks, Brigitte

Re: [Caml-list] recursive records

[Andreas Rossberg]

On Nov 8, 2013, at 21:10 , Brigitte Pientka <bpientka@cs.mcgill.ca> wrote:
> I am playing around with using recursive records to define observations about
> streams simulating essentially the ideas described in "Copatterns:Programming infinite structures by observations" presented at POPL'13.
> 
> type 'a susp = Susp of (unit -> 'a)
> 
> type 'a str = {hd: 'a  ; tl : ('a str) susp}
> 
> let rec ones = {hd = 1 ; tl = Susp (fun () -> ones)}
> 
> This works fine and many examples can be elegantly written this way.  However,
> when I define the stream ones via the function delay, OCaml fails.
> 
> let delay f = Susp f
> 
> let rec ones = {hd = 1 ; tl = delay (fun () -> ones)};;
> Characters 15-53:
>  let rec ones = {hd = 1 ; tl = delay (fun () -> ones)};;
>                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> Error: This kind of expression is not allowed as right-hand side of `let rec'
> 
> Could someone explain why this fails?

Roughly speaking, let rec only allows syntactic values as right-hand sides (to ease implementation and to avoid issues with potential observable side effects during tying of the recursive knot). An application like the one of delay is not a value. If you replace it by a direct application of the Susp constructor it should work.

/Andreas

Re: [Caml-list] recursive records

[Alain Frisch]

On 11/8/2013 9:17 PM, Andreas Rossberg wrote:
> An application like the one of delay is not a value.

One possible workaround for allowing such recursive bindings where 
references to the bound values are under abstractions which are not 
evaluated while tying the knot is to go through lazy values:

let ones =
  let rec ones = lazy {hd = 1; tl = delay (fun () -> Lazy.force ones)} in
  Lazy.force ones

(Of course, for this specific example, this is a little bit silly.)


-- Alain

Re: [Caml-list] recursive records

[oleg]

Brigitte Pientka wrote:

> type 'a susp = Susp of (unit -> 'a)
>
> type 'a str = {hd: 'a  ; tl : ('a str) susp}
>
> let rec ones = {hd = 1 ; tl = Susp (fun () -> ones)}
>
> This works fine and many examples can be elegantly written this way.  However,
> when I define the stream ones via the function delay, OCaml fails.
>
>   let delay f = Susp f
>    let rec ones = {hd = 1 ; tl = delay (fun () -> ones)};;
>                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> Error: This kind of expression is not allowed as right-hand side of `let rec'
>
> Could someone explain why this fails?

To be fair, OCaml already provides a few relaxations for let rec
definitions, which are described in Sec 7.3 of
        http://caml.inria.fr/pub/docs/manual-ocaml/extn.html
Alain Frisch has demonstrated one such extension: lazy.

I believe though there is a better way to represent your co-patterns
in OCaml -- using objects. Objects are already have a fix-points in
them, and objects are naturally coinductive: an object receives a
message, changes its state and results in an object ready for more
messages. The only think we can do with objects is to observe them,
but sending them messages. This sounds just like the definition of
co-induction. Here how it looks like:

(* defining the class type is not necessary, but helpful.
   It defines the type 'a str that is useful when writing signatures.
   I like to write signatures
*)
class type ['a] str = object ('self)
        method hd : 'a
        method tl : 'self
end;;

class ones = object (self) 
  method hd = 1
  method tl = self
end
;;

let ones = new ones;;

let take : int -> 'a str -> 'a list = fun n str ->
 let rec loop acc str = function
   | n when n <= 0 -> List.rev acc
   | n -> loop (str#hd :: acc) (str#tl) (n-1) (* Co-patterns! str#hd and str#tl *)
 in loop [] str n
;;

take 5 ones;;
   - : int list = [1; 1; 1; 1; 1]

Re: [Caml-list] recursive records

[Arkady Andrukonis]

[-- Attachment #1: Type: text/plain, Size: 2883 bytes --]

The "short" answer is the definition of 'delay' does not have a type associativity or bindings. For a recursive definition to work well, you would need to resolve into primitive types. When you try to accumulate a definition introducing more layers of complexity, one thing is just like this other (example, a candle is like a wax object with a wick), we see this every day with compound "of" metaphors, the type engine gets confused. You are using a constructor to define other items, therefore it fails. In natural languages you can get away with it, but not in programming languages.

Hope this helps.

Arkady





On Friday, November 8, 2013 11:02 PM, "oleg@okmij.org" <oleg@okmij.org> wrote:
 

Brigitte Pientka wrote:

> type 'a susp = Susp of (unit -> 'a)
>
> type 'a str = {hd: 'a  ; tl : ('a str) susp}
>
> let rec ones = {hd = 1 ; tl = Susp (fun () -> ones)}
>
> This works fine and many examples can be elegantly written this way.  However,
> when I define the stream ones via the function delay, OCaml fails.
>
>   let delay f = Susp f
>    let rec ones = {hd = 1 ; tl = delay (fun () -> ones)};;
>                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> Error: This kind of expression is not allowed as right-hand side of `let rec'
>
> Could someone explain why this fails?

To be fair, OCaml already provides a few relaxations for let rec
definitions, which are described in Sec 7.3 of
        http://caml.inria.fr/pub/docs/manual-ocaml/extn.html
Alain Frisch has demonstrated one such extension: lazy.

I believe though there is a better way to represent your co-patterns
in OCaml -- using objects. Objects are already have a fix-points in
them, and objects are naturally coinductive: an object receives a
message, changes its state and results in an object ready for more
messages. The only think we can do with objects is to observe them,
but sending them messages. This sounds just like the definition of
co-induction. Here how it looks like:

(* defining the class type is not necessary, but helpful.
   It defines the type 'a str that is useful when writing signatures.
   I like to write signatures
*)
class type ['a] str = object ('self)
        method hd : 'a
        method tl : 'self
end;;

class ones = object (self) 
  method hd = 1
  method tl = self
end
;;

let ones = new ones;;

let take : int -> 'a str -> 'a list = fun n str ->
let rec loop acc str = function
   | n when n <= 0 -> List.rev acc
   | n -> loop (str#hd :: acc) (str#tl) (n-1) (* Co-patterns! str#hd and str#tl *)
in loop [] str n
;;

take 5 ones;;
   - : int list = [1; 1; 1; 1; 1]



-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[-- Attachment #2: Type: text/html, Size: 5151 bytes --]