On Mon, 30 Jun 2003, Chris Hecker wrote:
> [Excellent rationale for private types snipped.]

Indeed. Nice feature. 

> >In contrast with abstract data types, the private types still maintain
> >the elegant pattern matching facility of ML outside the module that
> >defines the type.
> 
> So, when do we get views to solve this problem for abstract types?  If 
> pattern matching is so great (which it is) it seems a crime to not allow it 
> on abstract types (another great feature).  To make an american candy joke, 
> peanut butter and chocolate taste great together!

I guess we all know what you're going for when you hit that vending machine!

I was going to reply to a message in last week's thread about polytypic 
programming in which the use of open recursion/fixed points on functions was
demonstrated, that there is a "dual" trick at the level of types, the 
so-called two level types. One place this trick finds some use is in the 
encoding of views into ML like languages. You can find the trick demonstrated 
for SML here 

http://www.cs.princeton.edu/~danwang/drafts/recursion-schemes.pdf

but I'm not sure how much using this style costs in efficiency in OCaml. 
If it costs too much, we'll have to bug Stephen Weeks to implement OCamlton. 
BTW, it's nice to have views (and all kinds of things) supported directly in 
the language but these tricks seem workable to me. It seems like OCaml 
could be a bit nicer than SML here (what a surprise! :), since we could use 
polymorphic variants for the external interface, as there is no type 
abstraction there. For example, something like the following for the earliest 
examples in that paper 

module type NAT =
  sig
    type t
    type 'a s = [`Zero | `Succ of 'a]
    val inj : t s -> t
    val prj : t -> t s
  end

module SimpleNat : NAT =
  struct
    type 'a s = [`Zero | `Succ of 'a]

    (* Look ma, no intermediate constructor for recursive types! *)
    type t = t s

    let inj x = x
    let prj x = x
  end

module FastNat : NAT =
  struct
    type 'a s = [`Zero | `Succ of 'a]
    type t = int

    let inj = function
        `Zero -> 0
      | `Succ n -> n + 1

    let prj = function
        0 -> `Zero
      | n -> `Succ (n - 1)
  end

As a digression, the two level type trick is also used (in OCaml) here 

http://www.eecs.harvard.edu/~nr/pubs/mania-abstract.html
(This is a very appealing paper to me, as the embedded language technique the 
author describes looks applicable to a few things I'm doing) 

and here 

http://homepage.iis.sinica.edu.tw/~trc/padl00.ps

and of course in a ton of Haskell/Gofer/Squiggol oriented papers. 

As another digression, the trick of using open recursive functions and "fixing" 
them manually with special fps is explained nicely here:

 http://www.lfcs.informatics.ed.ac.uk/reports/97/ECS-LFCS-97-375/

though the post last week was the first time I saw it used in quite that way. 
That was quite neat. I wonder how that technique dovetails with two level 
types? 

-- Brian


-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners