Re: [Caml-list] Dependent types ?

["Jocelyn Sérot" <Jocelyn.SEROT@ubpmes.univ-bpclermont.fr>]

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

Thanks to all for your answers.

Phantom types could be a solution but we must declare a new type for  
each possible size, which is cumbersome / annoying.

Moreover, since i'm writing a DSL, the fact that they do not require a  
modification to the existing type system is not really an advantage.
My language has its own type system (largely inspired from OCaml's) so  
what I was looking for was more a way to modify the type  
representation to support the requested behavior.

To those familiar with Caml compiler source code, i was wondering if i  
could hack the following definitions (from types. ml)

type typ =
    | TyVar of typ_var
    | TyTerm of string * typ list

and typ_var =
   { mutable level: int;
     mutable value: tyvar_value }

and tyvar_value =
   | Unknown
   | Known of typ

by adding a notion of "size variable" (sorry if this sounds imprecise,  
this is still a but hazy in my mind..)

type typ =
    | TyVar of typ_var
    | TyTerm of string * typ list * typ_size

and typ_sz =
   { mutable value: tysz_value }

and tyvar_value =
   | Unknown
   | Known of int

and update the unification engine accordingly..

Well, the easiest answer is maybe just to try :-S
I'm just a bit surprised that no one seems to have proposed such an  
extension yet.

Jocelyn

Le 26 sept. 11 à 14:45, Yaron Minsky a écrit :

> As written, the behavior of the types might not be what you expect,  
> since addition of two 16 bit ints may result in an int that requires  
> 17 bits.
>
> When using phantom types, you need to be especially careful that the  
> types mean what you think they mean.
>
> On Sep 26, 2011 8:13 AM, "Denis Berthod" <denis.berthod@gmail.com>  
> wrote:
> > Hello,
> >
> > I think that achieving something very near from what you whant is
> > relatively easy using phantom types.
> > That avoid the boxing/unboxing in records.
> >
> > type i16
> > type i32
> >
> > module SizedInt:
> > sig
> > type 'a integer
> > val int16: int -> i16 integer
> > val int32: int -> i32 integer
> > val add: 'a integer -> 'a integer -> 'a integer
> > end
> > =
> > struct
> > type 'a integer = int
> >
> > let int16 x = x
> > let int32 x = x
> >
> > let add x y = x + y
> > end
> >
> > then
> >
> > open SizedInt
> >
> > let bar =
> > let x = int16 42 in
> > foo x
> >
> > must have type i16 integer -> i16 integer
> >
> > Regards,
> >
> > Denis Berthod
> >
> >
> > Le 26/09/2011 13:42, Jocelyn Sérot a écrit :
> >> Hello,
> >>
> >> I've recently come across a problem while writing a domain specific
> >> language for hardware synthesis
> >> (http://wwwlasmea.univ-bpclermont.fr/Personnel/Jocelyn.Serot/caph.html 
> ).
> >> The idea is to extend the type system to accept "size"  
> annotations for
> >> int types (it could equally apply to floats).
> >> The target language (VHDL in this case) accept "generic" functions,
> >> operating on ints with variable bit width and I'd like to reflect  
> this
> >> in the source language.
> >>
> >> For instance, I'd like to be able to declare :
> >>
> >> val foo : int * int -> int
> >>
> >> (where the type int is not annotated, i.e. "generic")
> >>
> >> so that, when applied to, let say :
> >>
> >> val x : int<16>
> >> val y : int<16>
> >>
> >> (where <16> is a size annotation),
> >>
> >> like in
> >>
> >> let z = foo (x,y)
> >>
> >> then the compiler will infer type int<16> for z
> >>
> >> In fact, the exact type signature for foo would be :
> >>
> >> val foo : int<s> * int <s> -> int<s>
> >>
> >> where "s" would be a "size variable" (playing a role similar to a  
> type
> >> variable in, for ex : val map : 'a list -> ('a ->'b) -> 'b list).
> >>
> >> In a sense, it has to do with the theory of sized types (Hughes and
> >> Paretto, .. ) and dependent types (DML for ex), but my goal is far
> >> less ambitious.
> >> In particular, i dont want to do _computations_ (1) on the size  
> (and,
> >> a fortiori, don't want to prove anything on the programs).
> >> So sized types / dependent types seems a big machinery for a
> >> relatively small goal.
> >> My intuition is that this is just a variant of polymorphism in  
> which
> >> the variables ranged over are not types but integers.
> >> Before testing this intuition by trying to implement it, I'd like  
> to
> >> know s/o has already tackled this problem.
> >> Any pointer - including "well, this is trivial" ! ;-) - will be
> >> appreciated.
> >>
> >> Best wishes
> >>
> >> Jocelyn
> >>
> >> (1) i.e. i dont bother supporting declarations like : val mul :  
> int<n>
> >> * int<n> -> int <2*n> ...
> >>
> >>
> >>
> >
> >
> > --
> > Caml-list mailing list. Subscription management and archives:
> > https://sympa-roc.inria.fr/wws/info/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: 9437 bytes --]