Re: [Caml-list] Dependent types ?

[Gabriel Scherer <gabriel.scherer@gmail.com>]

> 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>.

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
>>
>
>