Hello.
I've been struggling to have a type system where I could do the
following subtyping:
'a t1 :> t2 and t2 :> 'a t1
So I've tried to do the following:
yziq...@seldon:~$ ocaml
Objective Caml version 3.11.2
# #rectypes;;
# module Q = struct
type -'a e
type 'a q = privat
On Feb 27, 2010, at 02:52, Guillaume Yziquel wrote:
I've been struggling to have a type system where I could do the
following subtyping:
'a t1 :> t2 and t2 :> 'a t1
Hm, what do you mean? Subtyping ought to be reflexive and
antisymmetric (although the latter is rarely proved for most ty
Andreas Rossberg a écrit :
On Feb 27, 2010, at 02:52, Guillaume Yziquel wrote:
I've been struggling to have a type system where I could do the
following subtyping:
'a t1 :> t2 and t2 :> 'a t1
Hm, what do you mean? Subtyping ought to be reflexive and antisymmetric
(although the latter is
Guillaume Yziquel writes:
> Andreas Rossberg a écrit :
>> On Feb 27, 2010, at 02:52, Guillaume Yziquel wrote:
>>>
>>> I've been struggling to have a type system where I could do the
>>> following subtyping:
>>>
>>> 'a t1 :> t2 and t2 :> 'a t1
>>
>> Hm, what do you mean? Subtyping ought to be r
Goswin von Brederlow a écrit :
Guillaume Yziquel writes:
My goal is to implement a type inference barrier.
You can do
type 'a q = private w
and from the type inference point of view, int q and float q are two
distinct types, that you can subtype to a common type.
What I want is also to ha
On Feb 27, 2010, at 14:11, Guillaume Yziquel wrote:
# type q = private w and w = private q;;
type q = private w
and w = private q
# let f (x : q) = (x : q :> w);;
val f : q -> w =
# let f (x : q) = (x : w);;
Error: This expression has type q but an expression was expected of
type w
#
Intere
Andreas Rossberg a écrit :
On Feb 27, 2010, at 14:11, Guillaume Yziquel wrote:
# type q = private w and w = private q;;
type q = private w
and w = private q
# let f (x : q) = (x : q :> w);;
val f : q -> w =
# let f (x : q) = (x : w);;
Error: This expression has type q but an expression was expe
Guillaume Yziquel a écrit :
Andreas Rossberg a écrit :
On Feb 27, 2010, at 14:11, Guillaume Yziquel wrote:
# type q = private w and w = private q;;
type q = private w
and w = private q
# let f (x : q) = (x : q :> w);;
val f : q -> w =
# let f (x : q) = (x : w);;
Error: This expression has type
Guillaume Yziquel a écrit :
Guillaume Yziquel a écrit :
Andreas Rossberg a écrit :
On Feb 27, 2010, at 14:11, Guillaume Yziquel wrote:
# type q = private w and w = private q;;
type q = private w
and w = private q
# let f (x : q) = (x : q :> w);;
val f : q -> w =
# let f (x : q) = (x : w);;
Er
Guillaume Yziquel writes:
> Goswin von Brederlow a écrit :
>> Guillaume Yziquel writes:
>>
>>> My goal is to implement a type inference barrier.
>>>
>>> You can do
>>>
type 'a q = private w
>>> and from the type inference point of view, int q and float q are two
>>> distinct types, that yo
Goswin von Brederlow a écrit :
Doing 'a t = private underlying allows you to create a type inference
barrier. However, you also want to be able to cast from underlying to
'a t, when you get the result of a function in R or Python, for
instance.
So that's exactly the use case you mentionned abov
Guillaume Yziquel a écrit :
>> # type untyped;;
>> type untyped
>> # type 'a typed = private untyped;;
>> type 'a typed = private untyped
>> # type -'typing tau = private obj
>> and 'a t = 'a typed tau
>> and obj = private untyped tau;;
>> type 'a tau = private obj
>> and 'a t = 'a typed tau
>>
Stéphane Glondu a écrit :
Guillaume Yziquel a écrit :
# type untyped;;
type untyped
# type 'a typed = private untyped;;
type 'a typed = private untyped
# type -'typing tau = private obj
and 'a t = 'a typed tau
and obj = private untyped tau;;
type 'a tau = private obj
and 'a t = 'a typed tau
Guillaume Yziquel a écrit :
> Because subtyping seems more efficient than applying a noop function.
> And this code might run really often, so I do not like very much the
> idea of having noop functions running really often.
FWIW, I don't think you have any penalty if you declare your identities
a
Stéphane Glondu wrote:
> Guillaume Yziquel a écrit :
> > Because subtyping seems more efficient than applying a noop function.
> > And this code might run really often, so I do not like very much the
> > idea of having noop functions running really often.
>
> FWIW, I don't think you have any penal
Guillaume Yziquel wrote:
> Stéphane Glondu a écrit :
> > Guillaume Yziquel a écrit :
> >>> # type untyped;;
> >>> type untyped
> >>> # type 'a typed = private untyped;;
> >>> type 'a typed = private untyped
> >>> # type -'typing tau = private obj
> >>> and 'a t = 'a typed tau
> >>> and obj = pr
Stéphane Glondu a écrit :
Guillaume Yziquel a écrit :
Because subtyping seems more efficient than applying a noop function.
And this code might run really often, so I do not like very much the
idea of having noop functions running really often.
FWIW, I don't think you have any penalty if you d
"David Allsopp" writes:
> external foo_of_bar : bar -> foo = "%identity"
>
> in *both* the .ml and .mli file for the module in question. I'm virtually
> certain that ocamlopt eliminates calls to the %identity primitive.
Where is that documented? I would have written
let foo_of_bar (x : bar) =
David Allsopp a écrit :
Guillaume Yziquel wrote:
Stéphane Glondu a écrit :
Why don't you just declare 'a t to be synonym for obj in the
implementation of your module, declare them as abstract in its
interface, and export the specially typed identities f and g?
Because subtyping seems more ef
Goswin von Brederlow wrote:
> "David Allsopp" writes:
>
> > external foo_of_bar : bar -> foo = "%identity"
> >
> > in *both* the .ml and .mli file for the module in question. I'm
> virtually certain that ocamlopt eliminates calls to the %identity
> primitive.
>
> Where is that documented?
The u
Guillaume Yziquel wrote:
> David Allsopp a écrit :
> >
> > external foo_of_bar : bar -> foo = "%identity"
> >
> > in *both* the .ml and .mli file for the module in question. I'm
> virtually certain that ocamlopt eliminates calls to the %identity
> primitive.
>
> yziq...@seldon:~$ grep magic /usr/
"David Allsopp" writes:
> Goswin von Brederlow wrote:
>> "David Allsopp" writes:
>>
>> > external foo_of_bar : bar -> foo = "%identity"
>> >
>> > in *both* the .ml and .mli file for the module in question. I'm
>> virtually certain that ocamlopt eliminates calls to the %identity
>> primitive.
>>
22 matches
Mail list logo
