Simple(?) subtyping problem...

Simple(?) subtyping problem...

[Till Varoquaux]

I'm currently trying to split functions matching against given variant
type and I'm running across this pb:

let a= function
 | `A -> ()
 | `B -> ()

doesn't split into

let c=function
 | `B -> ()

let b =function
 | `A -> ()
 |  x -> c x

since it messes up the type rules. I really want to avoid having to
write down precise type informations (The point here is to have an
extensible system)...

I am sure this question has been asked loads of times (but I couldn't
find the right thread in the archives) and I apologize for asking it
yet again.

Till

Re: [Caml-list] Simple(?) subtyping problem...

[Jon Harrop]

On Tuesday 24 October 2006 21:45, Till Varoquaux wrote:
> I'm currently trying to split functions matching against given variant
> type and I'm running across this pb:
>
> let a= function
>
>  | `A -> ()
>  | `B -> ()
>
> doesn't split into
>
> let c=function
>
>  | `B -> ()
>
> let b =function
>
>  | `A -> ()
>  |  x -> c x
>
> since it messes up the type rules. I really want to avoid having to
> write down precise type informations (The point here is to have an
> extensible system)...

How about:

# type c = [`B];;
type c = [ `B ]
# let c = function
    | #c -> ();;
val c : [< c ] -> unit = <fun>
# let b k = function
    | `A -> ()
    | #c as x -> c x
    | x -> k x;; 
val b : (([> `A | `B ] as 'a) -> unit) -> 'a -> unit = <fun>

> I am sure this question has been asked loads of times (but I couldn't
> find the right thread in the archives) and I apologize for asking it
> yet again.

I don't think it comes up very often.

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
Objective CAML for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists

Re: [Caml-list] Simple(?) subtyping problem...

[Jacques Garrigue]

Slight variation on Jon's answer:

type c = [`B]

let c = function
| `B -> ()

let b = function
| `A -> ()
| #c as x -> c x

which has exactly the same type as your original b.

The way dispatching is typed in caml, you have to indicate explicitly
which cases you inherit from c. But it should no hinder extensibility.

Jacques Garrigue

From: "Till Varoquaux" <till.varoquaux@gmail.com>
> I'm currently trying to split functions matching against given variant
> type and I'm running across this pb:
> 
> let a= function
>  | `A -> ()
>  | `B -> ()
> 
> doesn't split into
> 
> let c=function
>  | `B -> ()
> 
> let b =function
>  | `A -> ()
>  |  x -> c x
> 
> since it messes up the type rules. I really want to avoid having to
> write down precise type informations (The point here is to have an
> extensible system)...
> 
> I am sure this question has been asked loads of times (but I couldn't
> find the right thread in the archives) and I apologize for asking it
> yet again.
> 
> Till

Re: [Caml-list] Simple(?) subtyping problem...

[Till Varoquaux]

This would work but it isn't an option since I cannot get it to work
with functors etc...
AFAIK there's no way to specify a type must be a polymorphic variant
without specfying any of it's members:

if we are building a functor against:

module type Evaluator=
sig
 ...
 type 'a exp (*Is an exact polymorphic variant type *)
 ...
end

we won't be able to write something like:

type 'a t=[ `Some_label of 'a | 'a exp ]

since the compiler won't be able to detect 'a exp was a polymorphic
variant (note: it looks like there could also be an issue on the
freshness of the new label)

trying to hack it like such:

module type Evaluator=
sig
 ...
 type 'a exp=[>`A_label of 'a ] (*Is an exact polymorphic variant type *)
 ...
end

won't work either....

As a final example I will put the code I'm trying to split in modules,
it seems to be a simple case raising lots questions, so here we go
(and I do know there are other ways to get my means...):

module type Evaluator=
sig
 type res
 type 'a exp
 val ops : ('a -> res) -> 'a exp -> res
 (*val eval : ('a exp as 'a) -> res*)
end


module Basic_ev: Evaluator=
 struct
  type res=int
  type 'a exp=[`Add of 'a * 'a | `Int of int | `Mul of 'a * 'a]

  let ops (eval:'a->res):('a exp -> res)  = function
   | `Int n -> n
   | `Add(e1, e2) -> eval e1 + eval e2
   | `Mul(e1, e2) -> eval e1 * eval e2

  let rec eval (e : 'a exp as 'a) : res=
   ops eval e

 end

module type Evaluator_extension=
 functor (Base:Evaluator)->(Evaluator with type res=Base.res)

module Advanced_ev : Evaluator_extension=
 functor(Base:(Evaluator with type res=int))->
  struct
   type res=int
   type 'a base= 'a Base.exp
   type 'a exp=[`Sub of 'a * 'a | 'a base ]

   let ops (eval:'a->res) :('a exp -> res) =
    function
    |`Sub(e1,e2) -> eval e1 - eval e2
    | #base as x -> Base.ops eval x

   let rec eval (e : 'a exp as 'a) : res=
    ops eval e
  end


Regards,
Till



On 10/25/06, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:
> Slight variation on Jon's answer:
>
> type c = [`B]
>
> let c = function
> | `B -> ()
>
> let b = function
> | `A -> ()
> | #c as x -> c x
>
> which has exactly the same type as your original b.
>
> The way dispatching is typed in caml, you have to indicate explicitly
> which cases you inherit from c. But it should no hinder extensibility.
>
> Jacques Garrigue
>
> From: "Till Varoquaux" <till.varoquaux@gmail.com>
> > I'm currently trying to split functions matching against given variant
> > type and I'm running across this pb:
> >
> > let a= function
> >  | `A -> ()
> >  | `B -> ()
> >
> > doesn't split into
> >
> > let c=function
> >  | `B -> ()
> >
> > let b =function
> >  | `A -> ()
> >  |  x -> c x
> >
> > since it messes up the type rules. I really want to avoid having to
> > write down precise type informations (The point here is to have an
> > extensible system)...
> >
> > I am sure this question has been asked loads of times (but I couldn't
> > find the right thread in the archives) and I apologize for asking it
> > yet again.
> >
> > Till
>

Re: [Caml-list] Simple(?) subtyping problem...

[Jacques Garrigue]

From: "Till Varoquaux" <till.varoquaux@gmail.com>

> This would work but it isn't an option since I cannot get it to work
> with functors etc...
> AFAIK there's no way to specify a type must be a polymorphic variant
> without specfying any of it's members:
> 
> if we are building a functor against:
> 
> module type Evaluator=
> sig
>  ...
>  type 'a exp (*Is an exact polymorphic variant type *)
>  ...
> end
> 
> we won't be able to write something like:
> 
> type 'a t=[ `Some_label of 'a | 'a exp ]
> 
> since the compiler won't be able to detect 'a exp was a polymorphic
> variant (note: it looks like there could also be an issue on the
> freshness of the new label)

There is indeed an issue of freshness :-)
There is code doing exactly what you ask for inside a branch in the
CVS for ocaml. The branch is still experimental, and is called
varunion.
You would have to write
  type 'a exp = private [> ] ~ [`Some_label of 'a]
    (* `Some_label may only have type 'a (if present) *)
or
  type 'a exp = private [> ] ~ [`Some_label of 'a]
    (* `Some_label is absent *)
in order to be able to use it later in combination with `Some_label.

You can look at the code in testlabl/varunion.ml, which includes
examples corresponding exactly to the code you are trying to write.

Jacques Garrigue