Copattern matching and first-class observations in OCaml, with a macro

Copattern matching and first-class observations in OCaml, with a macro, by Paul Laforgue and Yann Regis-Gianas:

Infinite data structures are elegantly defined by means of copattern matching, a dual construction to pattern matching that expresses the outcomes of the observations of an infinite structure. We extend the OCaml programming language with copatterns, exploiting the duality between pattern matching and copattern matching. Provided that a functional programming language has GADTs, every copattern matching can be transformed into a pattern matching via a purely local syntactic transformation, a macro. The development of this extension leads us to a generalization of previous calculus of copatterns: the introduction of first-class observation queries. We study this extension both from a formal and practical point of view.

Codata isn't well supported enough in languages IMO, and supporting it via a simple macro translation will hopefully make it easier to adopt, at least for any language with GADTs.

By naasking at 2017-09-26 15:13 | Admin | other blogs | 47179 reads

Examples from the paper

If you are like me, you like to look at code examples and try to guess what they do before you look at the details.

The first one computes the infinite stream of Fibonacci numbers.


type ‘a stream = {
  Head : ‘a ← ‘a stream;
  Tail : ‘a stream ← ‘a stream
}

(Note the arrows going left: these are projection functions for a record written in the other direction.)


let corec fib : int stream with
| ..#Head → 0
| ..#Tail#Head → 1
| ..#Tail#Tail → map2 (+) fib (fib#Tail)

Second example:

A fair bistream represents two streams of integers that must be consumed in a synchronized way. To enforce this fairness, the type index encodes the status of the head of each stream: it can be either read or unread.


type (‘a, ‘b) fbs = {
  Left : int ∗ (read, ‘b) fbs ← (unread, ‘b) fbs;
  Right : int ∗ (‘a, read) fbs ← (‘a, unread) fbs;
  BTail : (unread, unread) fbs ← (read, read) fbs;
}

Now the internal state of a bistream may be implemented by 2-buffers of the following type, with four possible states depending on the order in which its elements are consumed:


type (‘a, ‘b, ‘e) twobuffer =
| E : (read, read, ‘e) twobuffer
| L : ‘e → (unread, read, ‘e) twobuffer
| R : ‘e → (read, unread, ‘e) twobuffer
| F : ‘e ∗ ‘e → (unread, unread, ‘e) twobuffer


let corec zfrom : type a b.int → (a, b, int) twobuffer → (a, b) fbs with
| (..n E)#BTail          → zfrom (n + 1) (F (n, −n))
| (..n (L x))#Left       → (x, zfrom n E)
| (..n (F (x, y)))#Left  → (x, zfrom n (R y)))
| (..n (R x))#Right      → (x, zfrom n E)
| (..n (F (x, y)))#Right → (y, zfrom n (L x))

By gasche at Tue, 2017-09-26 15:44 | login or register to post comments