Re: [Caml-list] Dependent types ?

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

You're perfectly right Christophe,

I now realize that i've opened some kind of Pandora box.

Supporting function declaration

> concat : int<n> -> int<m> -> int<n+m> (or multiplication)

would be great  (even with only addition on sizes), but a too long  
term goal for me (esp. taking into account that i'm by no means a  
specialist in type theory !).

So, a simple approximation like

add : int<n> -> int<n> -> int<n>

(in which the size considerations are supposed to be handled at the  
VHDL level)

would be anough for me..

Jocelyn


Le 26 sept. 11 à 23:09, Christophe Raffalli a écrit :

> Hello,
>
> Le 26/09/11 18:44, Gabriel Scherer a écrit :
>>> Phantom types could be a solution but we must declare a new type for
>>> each possible size, which is cumbersome / annoying.
>> If you define the type system yourself, you can easily add a family  
>> of
>> type constants `size<n>` (with `n` an integer literal) to the default
>> environment of the type checker. Then you can define a parametrized
>> type `type 's sized_int` (or float, etc.) and instantiate it with any
>> of the size<n>.
> Another issue is if you wand function additionning size like
>
> concat : int<n> -> int<m> -> int<n+m> (or multiplication)
>
> and zext : int<n> -> int<m> (when m > n)
>
> Then your type system is likely to have to solve problems in  
> Pressburger
> arithmetics.
> Even only with existential quantifications, this is still not trivial
> (no elimination of quantifiers).
>
> But you could probably reuse the code of the Coq Omega tactics ... Or
> some other library
> like Facile, if you accept limited ranges for you sizes.
>
> I always wanted something like that for size of arrays in OCaml ...
>
> If you have no addition, then this is much easier... and if you have
> multiplication, this is likely to be undecidable
> (diophantian equations ...).
>
> So you should first list the functions you want with their types ...
>
> Regards,
> Christophe
>
> Which is decidable, but not trivial ...
>
>
>
>>
>> One issue with this minimal -- in term of modifications -- mechanism
>> is that you can represent meaningless types such as `float  
>> size_int` :
>> `float` is not a size. The canonical way to handle this is to add
>> a kind system on top of your type system, that would classify the
>> types into different kinds. Usual types would have kind `★`, and  
>> sizes
>> would have kind `Size`. You would then restrict the `'a` type  
>> variable in
>> `sized_int` to be of kind `Size`:
>>
>>  type ('a : Size) sized_int
>>
>> http://en.wikipedia.org/wiki/Kind_(type_theory)
>>
>> Remark: There is another useful way to combine kinds and sizes, which
>> is to use "sized kinds" to classify types whose memory representation
>> has a given size in your implementation. For example you would have
>> a kind `★` for types of one machine word, `★2` for two machine
>> words... This allows to keep parametric polymorphism in presence of
>> non-uniform representations, but it is restricted, less general, as
>> a given polymorphic definition would not quantify over all types, but
>> on all types of a given kind – unless you introduce kind  
>> polymorphism,
>> etc. It may be useful for typing low-level programs, but it doesn't
>> look like what you're looking for here.
>>
>>
>> On Mon, Sep 26, 2011 at 5:55 PM, Jocelyn Sérot
>> <Jocelyn.SEROT@ubpmes.univ-bpclermont.fr> wrote:
>>> 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
>>>>
>>>
>>
>
>
> -- 
> Christophe Raffalli
> Universite de Savoie
> Batiment Le Chablais, bureau 21
> 73376 Le Bourget-du-Lac Cedex
>
> tel: (33) 4 79 75 81 03
> fax: (33) 4 79 75 87 42
> mail: Christophe.Raffalli@univ-savoie.fr
> www: http://www.lama.univ-savoie.fr/~RAFFALLI
> ---------------------------------------------
> IMPORTANT: this mail is signed using PGP/MIME
> At least Enigmail/Mozilla, mutt or evolution
> can check this signature. The public key is
> stored on www.keyserver.net
> ---------------------------------------------
>
> <Christophe_Raffalli.vcf>