caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
* [Caml-list] Are record types generative?
@ 2018-01-23 14:54 Oleg
  2018-01-23 16:05 ` Jeremy Yallop
  0 siblings, 1 reply; 21+ messages in thread
From: Oleg @ 2018-01-23 14:54 UTC (permalink / raw)
  To: caml-list


I have recently received a rather odd type error:

       Type declarations do not match:
         type t = D.Product.t = { pid : int; name : string; price : int; }
       is not included in
         type t = RProduct.t = { pid : int; name : string; price : int; }

Apparently, two structurally identical record types are not regarded
equal (OCaml 4.04.0). The original code is a bit complicated, so
let me illustrate the problem on a simple example:

module type m1 = sig
  type t = int
  val v : t
end

module M1 : m1 = struct
  type t = int
  let v = 1
end

module F1(S:m1) = struct
  let res = S.v = M1.v
end

let _ = let module M = F1(M1) in M.res;;

This code is accepted with no problems and gives the expected result
(1 is indeed equal to 1). Module M1 was checked to satisfy the
signature m1; therefore, S.v and M1.v should have the type int and be
the same.

Let's change the example slightly

module type m2 = sig
  type t = {l:int}
  val v : t
end

module M2 : m2 = struct
  type t = {l:int}
  let v = {l=1}
end

module F2(S:m2) = struct
  let res = S.v = M2.v
end

  Characters 43-47:
    let res = S.v = M2.v
                    ^^^^
Error: This expression has type M2.t but an expression was expected of type
         S.t

Although both M2 and S are two instances of m2, and hence both
S.v and M2.v  should have the record type t = {l:int}, they are not
regarded equal.

The problem is easy to fix:

module F3(S:m2 with type t = M2.t) = struct
  let res = S.v = M2.v
end
;;

  module F3 :
  functor (S : sig type t = M2.t = { l : int; } val v : t end) ->
    sig val res : bool end

let _ = let module M = F3(M2) in M.res;;

but even in this simple case the fix is ugly (and becomes uglier in
the real code). Maybe there is a way to avoid adding too many sharing
constraints?

BTW, the new manual has a section about common polymorphism
pitfalls. Modules also have a fair share of dark corners (along with
the objects). Perhaps there could be a section in the manual about
not so obvious aspects of modules (in the first approximation,
just collecting questions and answers like the present one).




^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-23 14:54 [Caml-list] Are record types generative? Oleg
@ 2018-01-23 16:05 ` Jeremy Yallop
  2018-01-23 17:39   ` Chet Murthy
  0 siblings, 1 reply; 21+ messages in thread
From: Jeremy Yallop @ 2018-01-23 16:05 UTC (permalink / raw)
  To: Oleg, Caml List

On 23 January 2018 at 14:54, Oleg <oleg@okmij.org> wrote:
> Although both M2 and S are two instances of m2, and hence both
> S.v and M2.v  should have the record type t = {l:int}, they are not
> regarded equal.

Yes: record definitions are indeed generative in OCaml, unlike in Standard ML.

> The problem is easy to fix:
>
> module F3(S:m2 with type t = M2.t) = struct
>   let res = S.v = M2.v
> end
> ;;
>
>   module F3 :
>   functor (S : sig type t = M2.t = { l : int; } val v : t end) ->
>     sig val res : bool end
>
> let _ = let module M = F3(M2) in M.res;;
>
> but even in this simple case the fix is ugly (and becomes uglier in
> the real code). Maybe there is a way to avoid adding too many sharing
> constraints?

One approach is to ensure that record and variant declarations do not
appear in signatures, so that type members in signatures are just
equations that refer to top-level types.  Then your example could be
written like this:

    type s = {l:int}

    module type m2 = sig
      type t = s
      val v : t
    end

    module M2 : m2 = struct
      type t = s
      let v = {l=1}
    end

    module F2(S:m2) = struct
      let res = S.v = M2.v
    end

Things become a little trickier if the type definition refers to other
elements in the signature

   module type m3 = sig
      type a
      type t = {l:a}
       ...

Losing equalities between different instances of 't' may in fact be
the desired behaviour here, since 'a' can be instantiated differently
in each implementation of the module.  But if it's important to keep
equalities then parameterising the record can help:

   type 'b s = {l:'b}

   module type m3 = sig
      type a
      type t = a s
       ...

> BTW, the new manual has a section about common polymorphism
> pitfalls. Modules also have a fair share of dark corners (along with
> the objects). Perhaps there could be a section in the manual about
> not so obvious aspects of modules (in the first approximation,
> just collecting questions and answers like the present one).

I think that'd be very useful.

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-23 16:05 ` Jeremy Yallop
@ 2018-01-23 17:39   ` Chet Murthy
  2018-01-23 20:35     ` Jeremy Yallop
  0 siblings, 1 reply; 21+ messages in thread
From: Chet Murthy @ 2018-01-23 17:39 UTC (permalink / raw)
  To: Jeremy Yallop; +Cc: Oleg, Caml List

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

The generativity of record types is, I believe, one of the key prereqs for
achieving a decidable type inference algorithm in the absence of any type
annotations, in caml.  That is, when you write a caml program and it fails
to type-check, you can't make it type-check by adding "enough"
type-annotations.  For a programmer, this is critical -- when the compiler
tells you that your program doesn't type-check, it means that your code is
actually broken.  Whereas in SML/NJ, you might need to add some more
type-annotations.

It was one of the things that convinced me to switch to caml, lo these many
decades.

On Tue, Jan 23, 2018 at 8:05 AM, Jeremy Yallop <yallop@gmail.com> wrote:

>
> Yes: record definitions are indeed generative in OCaml, unlike in Standard
> ML.
>

[-- Attachment #2: Type: text/html, Size: 1131 bytes --]

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-23 17:39   ` Chet Murthy
@ 2018-01-23 20:35     ` Jeremy Yallop
  2018-01-23 21:36       ` Chet Murthy
  0 siblings, 1 reply; 21+ messages in thread
From: Jeremy Yallop @ 2018-01-23 20:35 UTC (permalink / raw)
  To: Chet Murthy; +Cc: Oleg, Caml List

On 23 January 2018 at 17:39, Chet Murthy <murthy.chet@gmail.com> wrote:
> That is, when you write a caml program and it fails to type-check, you can't make it type-check by adding "enough" type-annotations.

This hasn't been the case for a long time (perhaps ever), and it's
becoming less true with each release.  For example, all of the
following programs pass type checking as written, but are rejected if
the annotations are removed:

   (* 1 *)   let f (g : x:int -> y:int -> int) x y = (g ~x ~y, g ~y ~x)
   (* 2 *)   let rec f : 'a. 'a -> unit = fun x -> ignore (f 3, f "four")
   (* 3 *)   let f : [`A] -> unit = function `A -> () | _ -> .
   (* 4 *)   module type S = module type of struct let r : int list
ref = ref [] end
   (* 5 *)   let f (o : <m:'a.'a -> unit>) = (o#m (), o#m 2)
   (* 6 *)   let f z = let rec x = [| y; z |] and y : int = z in x
   (* 7 *)   let x : _ format6 = "%d" in Printf.sprintf x
   (* 8 *)   type a = A | B   type b = A   let x = (A : a) = B
   (* 9 *)   let f : (module S) = (module struct end)
   (* 10 *) module rec M : module type of struct let f : int -> int =
assert false end = struct let f = M.f end

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-23 20:35     ` Jeremy Yallop
@ 2018-01-23 21:36       ` Chet Murthy
  2018-01-23 22:06         ` Jeremy Yallop
  0 siblings, 1 reply; 21+ messages in thread
From: Chet Murthy @ 2018-01-23 21:36 UTC (permalink / raw)
  To: Jeremy Yallop; +Cc: Oleg, Caml List

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

Heh. I was careful to say "caml", not "ocaml".   I'm aware that polymorphic
variants, objects, and (heh, I forgot) labels all violate the rule. And of
course, modules do.

Like I said: *caml* has this property.  Certainly caml-light, circa 1993
did, IIRC.

I remember having a nice discussion with Pierre Weis, where I asked him why
record-labels were generative, and he pointed this out to me.

--chet--


On Tue, Jan 23, 2018 at 12:35 PM, Jeremy Yallop <yallop@gmail.com> wrote:

> On 23 January 2018 at 17:39, Chet Murthy <murthy.chet@gmail.com> wrote:
> > That is, when you write a caml program and it fails to type-check, you
> can't make it type-check by adding "enough" type-annotations.
>
> This hasn't been the case for a long time (perhaps ever), and it's
> becoming less true with each release.  For example, all of the
> following programs pass type checking as written, but are rejected if
> the annotations are removed:
>
>    (* 1 *)   let f (g : x:int -> y:int -> int) x y = (g ~x ~y, g ~y ~x)
>    (* 2 *)   let rec f : 'a. 'a -> unit = fun x -> ignore (f 3, f "four")
>    (* 3 *)   let f : [`A] -> unit = function `A -> () | _ -> .
>    (* 4 *)   module type S = module type of struct let r : int list
> ref = ref [] end
>    (* 5 *)   let f (o : <m:'a.'a -> unit>) = (o#m (), o#m 2)
>    (* 6 *)   let f z = let rec x = [| y; z |] and y : int = z in x
>    (* 7 *)   let x : _ format6 = "%d" in Printf.sprintf x
>    (* 8 *)   type a = A | B   type b = A   let x = (A : a) = B
>    (* 9 *)   let f : (module S) = (module struct end)
>    (* 10 *) module rec M : module type of struct let f : int -> int =
> assert false end = struct let f = M.f end
>

[-- Attachment #2: Type: text/html, Size: 2341 bytes --]

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-23 21:36       ` Chet Murthy
@ 2018-01-23 22:06         ` Jeremy Yallop
  2018-01-23 23:14           ` Hendrik Boom
  2018-01-24  1:05           ` Chet Murthy
  0 siblings, 2 replies; 21+ messages in thread
From: Jeremy Yallop @ 2018-01-23 22:06 UTC (permalink / raw)
  To: Chet Murthy; +Cc: Oleg, Caml List

On 23 January 2018 at 21:36, Chet Murthy <murthy.chet@gmail.com> wrote:
> Heh. I was careful to say "caml", not "ocaml".   I'm aware that polymorphic
> variants, objects, and (heh, I forgot) labels all violate the rule. And of
> course, modules do.
>
> Like I said: *caml* has this property.  Certainly caml-light, circa 1993
> did, IIRC.

I think people usually consider OCaml an implementation of Caml.
(See, e.g. the documentation at http://caml.inria.fr/)

Of course, you're quite right that most of these programs weren't
valid in caml light.  But even (later versions of) caml light had
format strings with string syntax, so it was possible to write
programs that were rejected without annotations and accepted with
annotations.

In any case, whether annotations can be erased without affecting type
correctness is an interesting property to consider.  Here's a closely
related property that's much harder to break: does adding annotations
leave the run-time behaviour of a program unchanged?  There are far
fewer programs that violate that property, I think.

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-23 22:06         ` Jeremy Yallop
@ 2018-01-23 23:14           ` Hendrik Boom
  2018-01-24  1:06             ` Chet Murthy
                               ` (2 more replies)
  2018-01-24  1:05           ` Chet Murthy
  1 sibling, 3 replies; 21+ messages in thread
From: Hendrik Boom @ 2018-01-23 23:14 UTC (permalink / raw)
  To: caml-list

On Tue, Jan 23, 2018 at 10:06:55PM +0000, Jeremy Yallop wrote:
> 
> In any case, whether annotations can be erased without affecting type
> correctness is an interesting property to consider.  Here's a closely
> related property that's much harder to break: does adding annotations
> leave the run-time behaviour of a program unchanged?  There are far
> fewer programs that violate that property, I think.

I'm starting to think that the ability to write OCaml programs without 
mentioning the types is a drawback in the language, because it makes 
programs hard to understand.

-- hendrik

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-23 22:06         ` Jeremy Yallop
  2018-01-23 23:14           ` Hendrik Boom
@ 2018-01-24  1:05           ` Chet Murthy
  2018-01-24  8:43             ` Jacques Garrigue
  1 sibling, 1 reply; 21+ messages in thread
From: Chet Murthy @ 2018-01-24  1:05 UTC (permalink / raw)
  To: Jeremy Yallop; +Cc: Oleg, Caml List

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

On Tue, Jan 23, 2018 at 2:06 PM, Jeremy Yallop <yallop@gmail.com> wrote:
>
> IHere's a closely
> related property that's much harder to break: does adding annotations
> leave the run-time behaviour of a program unchanged?  There are far
> fewer programs that violate that property, I think.
>

I'm no longer a type-theorist, so I don't have the knowledge to answer, but:

It was a critically important property of *all* the original MLs (and of
the theoretical development of ML) that a well-type ML program P could be
"type-erased" to an untyped program TE(P); then when P -eval-> V, and TE(P)
-eval-> V', TE(V) == V'.  Where's I'm abusing notation, b/c "-eval->" means
in the first case "evaluation on typed programs" and in the second,
"evaluation on untyped programs" which might be entirely different things.

This was the (famous amongst that admittedly tiny community) "commuting
rectangles type erasure property".

A -concrete- effect of this property in MLs (again, I'm no longer a
type-theorist, so I might be getting this wrong) is ML-family languages
don't support reflection, and when they support object-orientation, they
don't support "instanceof" (e.g. like Java's).  because these require that
compile-time type-information be present at runtime.

For those who think this is a bad design choice, I can only say that as a
systems-jock, I appreciate a language that is -so- high-level, and -yet-
can easily be programmed in such a way that I can understand the runtime
behaviour in terms of a C-like runtime model.  By contrast, to understand
Java *for real* one must have enormously detailed knowledge of the JVM --
the particular JVM implementation -- one is using.

--chet--

[-- Attachment #2: Type: text/html, Size: 2534 bytes --]

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-23 23:14           ` Hendrik Boom
@ 2018-01-24  1:06             ` Chet Murthy
  2018-01-24  1:35             ` Francois BERENGER
  2018-01-24  1:56             ` [Caml-list] Are record types generative? Yawar Amin
  2 siblings, 0 replies; 21+ messages in thread
From: Chet Murthy @ 2018-01-24  1:06 UTC (permalink / raw)
  To: Hendrik Boom; +Cc: caml-list

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

Of course, you are *always* free to add whatever type-annotations you wish
to your program.  But the program's correctness cannot be affected by them
(well, again, for the archaic subset of ocaml extant in ... 1992).  --chet--

On Tue, Jan 23, 2018 at 3:14 PM, Hendrik Boom <hendrik@topoi.pooq.com>
wrote:\
>
>
> I'm starting to think that the ability to write OCaml programs without
> mentioning the types is a drawback in the language, because it makes
> programs hard to understand.\
>

[-- Attachment #2: Type: text/html, Size: 824 bytes --]

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-23 23:14           ` Hendrik Boom
  2018-01-24  1:06             ` Chet Murthy
@ 2018-01-24  1:35             ` Francois BERENGER
  2018-02-07  2:00               ` [Caml-list] [ANN] first release of bst: a bisector tree implementation Francois BERENGER
  2018-01-24  1:56             ` [Caml-list] Are record types generative? Yawar Amin
  2 siblings, 1 reply; 21+ messages in thread
From: Francois BERENGER @ 2018-01-24  1:35 UTC (permalink / raw)
  To: caml-list

On 01/24/2018 08:14 AM, Hendrik Boom wrote:
> I'm starting to think that the ability to write OCaml programs without 
> mentioning the types is a drawback in the language, because it makes 
> programs hard to understand.

It is a decisive advantage of the language when prototyping software
(i.e. all the work before you decide to engrave a .mli file on a stone).

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-23 23:14           ` Hendrik Boom
  2018-01-24  1:06             ` Chet Murthy
  2018-01-24  1:35             ` Francois BERENGER
@ 2018-01-24  1:56             ` Yawar Amin
  2018-01-25 10:49               ` Matej Košík
  2 siblings, 1 reply; 21+ messages in thread
From: Yawar Amin @ 2018-01-24  1:56 UTC (permalink / raw)
  To: Hendrik Boom; +Cc: Ocaml Mailing List

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

Hi,

On Tue, Jan 23, 2018 at 6:14 PM, Hendrik Boom <hendrik@topoi.pooq.com>
wrote:

> I'm starting to think that the ability to write OCaml programs without
> mentioning the types is a drawback in the language, because it makes
> programs hard to understand.
>

 It's a tooling issue. If your editor can show you type hints and jump to
definitions on demand, you no longer have this problem. Yes, you still
can't see the types while the code is on GitHub, but that is not
insurmountable. Browser extensions nowadays are perfectly capable of
downloading and locally storing typing information and displaying it on
hover. I believe the tooling will be built when the need is acute enough.

[-- Attachment #2: Type: text/html, Size: 1098 bytes --]

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-24  1:05           ` Chet Murthy
@ 2018-01-24  8:43             ` Jacques Garrigue
  2018-02-02 23:07               ` Toby Kelsey
  0 siblings, 1 reply; 21+ messages in thread
From: Jacques Garrigue @ 2018-01-24  8:43 UTC (permalink / raw)
  To: Chet Murthy; +Cc: Jeremy Yallop, Oleg Kiselyov, Mailing List OCaml

On 2018/01/24 10:05, Chet Murthy wrote:
> 
> On Tue, Jan 23, 2018 at 2:06 PM, Jeremy Yallop <yallop@gmail.com> wrote:
> IHere's a closely
> related property that's much harder to break: does adding annotations
> leave the run-time behaviour of a program unchanged?  There are far
> fewer programs that violate that property, I think.
> 
> I'm no longer a type-theorist, so I don't have the knowledge to answer, but:
> 
> It was a critically important property of *all* the original MLs (and of the theoretical development of ML) that a well-type ML program P could be "type-erased" to an untyped program TE(P); then when P -eval-> V, and TE(P) -eval-> V', TE(V) == V'.  Where's I'm abusing notation, b/c "-eval->" means in the first case "evaluation on typed programs" and in the second, "evaluation on untyped programs" which might be entirely different things.
> 
> This was the (famous amongst that admittedly tiny community) "commuting rectangles type erasure property”.

This property is still true in OCaml (minus Obj.magic, but Obj.magic is not valid OCaml :-).
I.e., types can be used to optimize a program, but they do not change its semantics.
It’s true of so-called “overloaded” record labels, it’s true of a labeled and default arguments
(which use type information for compilation, but not semantics), it’s true of objects,
 it’s true of GADT pattern-matching (again optimized), etc…

> A -concrete- effect of this property in MLs (again, I'm no longer a type-theorist, so I might be getting this wrong) is ML-family languages don't support reflection, and when they support object-orientation, they don't support "instanceof" (e.g. like Java's).  because these require that compile-time type-information be present at runtime.

Indeed, as soon as we add type classes, type witnesses or (type-selected) implicit arguments, this property is lost.

> For those who think this is a bad design choice, I can only say that as a systems-jock, I appreciate a language that is -so- high-level, and -yet- can easily be programmed in such a way that I can understand the runtime behaviour in terms of a C-like runtime model.  By contrast, to understand Java *for real* one must have enormously detailed knowledge of the JVM -- the particular JVM implementation -- one is using.


Indeed.

Jacques

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-24  1:56             ` [Caml-list] Are record types generative? Yawar Amin
@ 2018-01-25 10:49               ` Matej Košík
  2018-01-25 13:39                 ` Simon Cruanes
  2018-01-25 16:24                 ` Yawar Amin
  0 siblings, 2 replies; 21+ messages in thread
From: Matej Košík @ 2018-01-25 10:49 UTC (permalink / raw)
  To: caml-list

Hi

On 01/24/18 02:56, Yawar Amin wrote:
> Hi,
> 
> On Tue, Jan 23, 2018 at 6:14 PM, Hendrik Boom <hendrik@topoi.pooq.com <mailto:hendrik@topoi.pooq.com>> wrote:
> 
>     I'm starting to think that the ability to write OCaml programs without
>     mentioning the types is a drawback in the language, because it makes
>     programs hard to understand.
> 
> 
>  It's a tooling issue.

It very much depends on what you (honestly) care about.

If you do not care about readability of the programs you write, then it is "tooling issue"
(like in "Use Merlin bro!")

If you care about readability, then ephemeral Merlin (or whatever) tooltips are not exactly the same stuff
as type information that is directly, permanently, unconditionally present in the source code.

From the reader's point of view, it is not the same thing, really.

In addition to that, when one uses polymorphic variants heavily,
the presence or absence of typing annotations makes a drastic impact on the ability of typing errors the compiler can generate.

From the programmer's point of view (who has to deal with typing errors when they happen), it is not the same thing, really.

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-25 10:49               ` Matej Košík
@ 2018-01-25 13:39                 ` Simon Cruanes
  2018-01-25 16:24                 ` Yawar Amin
  1 sibling, 0 replies; 21+ messages in thread
From: Simon Cruanes @ 2018-01-25 13:39 UTC (permalink / raw)
  To: Matej Košík, caml-list

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

Note that you can explicitly annotate function types (possibly with _ at some places when full types would be too long or are irrelevant). I've been doing it more and more recently and it's really readable. 
-- 
Simon (from my phone) 

[-- Attachment #2: Type: text/html, Size: 252 bytes --]

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-25 10:49               ` Matej Košík
  2018-01-25 13:39                 ` Simon Cruanes
@ 2018-01-25 16:24                 ` Yawar Amin
  1 sibling, 0 replies; 21+ messages in thread
From: Yawar Amin @ 2018-01-25 16:24 UTC (permalink / raw)
  To: Matej Košík; +Cc: Ocaml Mailing List

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

Hello,

On Thu, Jan 25, 2018 at 5:49 AM, Matej Košík <mail@matej-kosik.net> wrote:

> [...]
> It very much depends on what you (honestly) care about.
>
> If you do not care about readability of the programs you write, then it is
> "tooling issue"
> (like in "Use Merlin bro!")
>

Readability means different things to everyone. There's no guaranteed
recipe for achieving it. Ultimately, it's one of those things that, you'll
know it when you see it.

It's true though, Merlin is also not the tool that will solve everything
for everyone. There's no substitute for building your own mental model of
the code as you read it.

If you care about readability, then ephemeral Merlin (or whatever) tooltips
> are not exactly the same stuff
> as type information that is directly, permanently, unconditionally present
> in the source code.
>

In OCaml, two things really aid in readability: it's idiomatic to use
module prefixes, and it's idiomatic to provide interface files with full
typing information. Anyone who is reading the code seriously can use those
to boost their understanding.

From the reader's point of view, it is not the same thing, really.
>

The thing is, there are different kinds of readers with different needs.
When you are a newcomer to the codebase, you need more help to understand
what's going on. But (hopefully) as you get more and more familiar with it,
which should be the majority of the time you spend reading it, you don't
need all the noise of typing information in implementation files. You
already have a model of what the types are and if you're unclear about
something, you have everything I mentioned before as well as being able to
just run quick experiments and seeing what errors the typechecker gives you.

In addition to that, when one uses polymorphic variants heavily,
> the presence or absence of typing annotations makes a drastic impact on
> the ability of typing errors the compiler can generate.
>

Sure, it's really helpful to hint to the compiler what kinds of errors it
should report. But this is not a common use case–the compiler is actually
pretty good at inferring basic nominal types.

[-- Attachment #2: Type: text/html, Size: 3067 bytes --]

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-01-24  8:43             ` Jacques Garrigue
@ 2018-02-02 23:07               ` Toby Kelsey
  2018-02-02 23:23                 ` Evgeny Roubinchtein
  2018-02-04  1:27                 ` Jacques Garrigue
  0 siblings, 2 replies; 21+ messages in thread
From: Toby Kelsey @ 2018-02-02 23:07 UTC (permalink / raw)
  To: caml-list

On 24/01/18 08:43, Jacques Garrigue wrote:
> I.e., types can be used to optimize a program, but they do not change its semantics.
> It’s true of so-called “overloaded” record labels, it’s true of a labeled and default arguments
> (which use type information for compilation, but not semantics), it’s true of objects,
>   it’s true of GADT pattern-matching (again optimized), etc…

type foo = { x : int }
type bar = { x : string }

let f r = r.x           (* OK: uses bar *)
let f r = (r:foo).x  (* OK: uses foo *)
let f r = (r.x : int) (* type error - wrong type inferred *)


Aren't the semantics different? 'f' has different types in the first two definitions, And why does type inference fail 
for the last example?

Toby

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-02-02 23:07               ` Toby Kelsey
@ 2018-02-02 23:23                 ` Evgeny Roubinchtein
  2018-02-04  1:27                 ` Jacques Garrigue
  1 sibling, 0 replies; 21+ messages in thread
From: Evgeny Roubinchtein @ 2018-02-02 23:23 UTC (permalink / raw)
  To: Toby Kelsey; +Cc: OCaml Mailing List

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

One source that explains how record labels are disambiguated is:
https://realworldocaml.org/v1/en/html/records.html#reusing-field-names.

Parenthetically, it seems to me that your question is hardly related to the
subject of this thread, so it may have been better to start a new thread in
this case, than to piggy-back onto an existing thread.

-- 
Best,
Evgeny ("Zhenya")

On Fri, Feb 2, 2018 at 3:07 PM, Toby Kelsey <toby.kelsey@gmail.com> wrote:

> On 24/01/18 08:43, Jacques Garrigue wrote:
>
>> I.e., types can be used to optimize a program, but they do not change its
>> semantics.
>> It’s true of so-called “overloaded” record labels, it’s true of a labeled
>> and default arguments
>> (which use type information for compilation, but not semantics), it’s
>> true of objects,
>>   it’s true of GADT pattern-matching (again optimized), etc…
>>
>
> type foo = { x : int }
> type bar = { x : string }
>
> let f r = r.x           (* OK: uses bar *)
> let f r = (r:foo).x  (* OK: uses foo *)
> let f r = (r.x : int) (* type error - wrong type inferred *)
>
>
> Aren't the semantics different? 'f' has different types in the first two
> definitions, And why does type inference fail for the last example?
>
> Toby
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/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: 2530 bytes --]

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] Are record types generative?
  2018-02-02 23:07               ` Toby Kelsey
  2018-02-02 23:23                 ` Evgeny Roubinchtein
@ 2018-02-04  1:27                 ` Jacques Garrigue
  1 sibling, 0 replies; 21+ messages in thread
From: Jacques Garrigue @ 2018-02-04  1:27 UTC (permalink / raw)
  To: Toby Kelsey; +Cc: Mailing List OCaml

On 2018/02/03 08:07, Toby Kelsey wrote:
> 
> On 24/01/18 08:43, Jacques Garrigue wrote:
>> I.e., types can be used to optimize a program, but they do not change its semantics.
>> It’s true of so-called “overloaded” record labels, it’s true of a labeled and default arguments
>> (which use type information for compilation, but not semantics), it’s true of objects,
>>  it’s true of GADT pattern-matching (again optimized), etc…
> 
> type foo = { x : int }
> type bar = { x : string }
> 
> let f r = r.x           (* OK: uses bar *)
> let f r = (r:foo).x  (* OK: uses foo *)
> let f r = (r.x : int) (* type error - wrong type inferred *)
> 
> 
> Aren't the semantics different? 'f' has different types in the first two definitions, And why does type inference fail for the last example?


By semantics, I mean runtime semantics (i.e. the evaluation of a program).
The first two functions both return the contents of the field x of their argument.
The problem with the 3rd function is not semantics but incompleteness of type inference in presence of label overloading.

Jacques

^ permalink raw reply	[flat|nested] 21+ messages in thread

* [Caml-list] [ANN] first release of bst: a bisector tree implementation
  2018-01-24  1:35             ` Francois BERENGER
@ 2018-02-07  2:00               ` Francois BERENGER
  2018-02-07 12:40                 ` Ivan Gotovchits
  0 siblings, 1 reply; 21+ messages in thread
From: Francois BERENGER @ 2018-02-07  2:00 UTC (permalink / raw)
  To: caml-list

Hello,

A bisector tree allows to do fast but exact nearest neighbor searches in
any space provided that you have a metric (function) to measure the
distance between any two points in that space.

It also allows proximity queries, as in "all points within distance d
from my query point".

Cf. this article for details: "A Data Structure and an Algorithm for the
Nearest Point Problem"; Iraj Kalaranti and Gerard McDonald.
ieeexplore.ieee.org/iel5/32/35936/01703102.pdf

The code is here:
https://github.com/UnixJunkie/bisec-tree

It might interest users of vantage point trees (minivpt, and vpt in
opam), kd-trees and such.
I think bst should be faster than vpt in most use cases.

It should appear in opam shortly.

Regards,
Francois.


^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] [ANN] first release of bst: a bisector tree implementation
  2018-02-07  2:00               ` [Caml-list] [ANN] first release of bst: a bisector tree implementation Francois BERENGER
@ 2018-02-07 12:40                 ` Ivan Gotovchits
  2018-02-08  0:46                   ` Francois BERENGER
  0 siblings, 1 reply; 21+ messages in thread
From: Ivan Gotovchits @ 2018-02-07 12:40 UTC (permalink / raw)
  To: Francois BERENGER; +Cc: caml-list

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

Hi,

Thanks for the excellent contribution, that's really useful. But can you
please provide a license to use it? Something like MIT would be awesome!

Cheers,
Ivan Gotovchits

On Feb 6, 2018 9:00 PM, "Francois BERENGER" <berenger@bioreg.kyushu-u.ac.jp>
wrote:

> Hello,
>
> A bisector tree allows to do fast but exact nearest neighbor searches in
> any space provided that you have a metric (function) to measure the
> distance between any two points in that space.
>
> It also allows proximity queries, as in "all points within distance d
> from my query point".
>
> Cf. this article for details: "A Data Structure and an Algorithm for the
> Nearest Point Problem"; Iraj Kalaranti and Gerard McDonald.
> ieeexplore.ieee.org/iel5/32/35936/01703102.pdf
>
> The code is here:
> https://github.com/UnixJunkie/bisec-tree
>
> It might interest users of vantage point trees (minivpt, and vpt in
> opam), kd-trees and such.
> I think bst should be faster than vpt in most use cases.
>
> It should appear in opam shortly.
>
> Regards,
> Francois.
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/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: 2289 bytes --]

^ permalink raw reply	[flat|nested] 21+ messages in thread

* Re: [Caml-list] [ANN] first release of bst: a bisector tree implementation
  2018-02-07 12:40                 ` Ivan Gotovchits
@ 2018-02-08  0:46                   ` Francois BERENGER
  0 siblings, 0 replies; 21+ messages in thread
From: Francois BERENGER @ 2018-02-08  0:46 UTC (permalink / raw)
  To: caml-list

On 02/07/2018 09:40 PM, Ivan Gotovchits wrote:
> Hi,
> 
> Thanks for the excellent contribution, that's really useful. But can you
> please provide a license to use it? Something like MIT would be awesome!

The license is BSD-3, it is only said in the opam package, sorry.
I'll add a license file into the repository.

> Cheers,
> Ivan Gotovchits
> 
> On Feb 6, 2018 9:00 PM, "Francois BERENGER"
> <berenger@bioreg.kyushu-u.ac.jp <mailto:berenger@bioreg.kyushu-u.ac.jp>>
> wrote:
> 
>     Hello,
> 
>     A bisector tree allows to do fast but exact nearest neighbor searches in
>     any space provided that you have a metric (function) to measure the
>     distance between any two points in that space.
> 
>     It also allows proximity queries, as in "all points within distance d
>     from my query point".
> 
>     Cf. this article for details: "A Data Structure and an Algorithm for the
>     Nearest Point Problem"; Iraj Kalaranti and Gerard McDonald.
>     ieeexplore.ieee.org/iel5/32/35936/01703102.pdf
>     <http://ieeexplore.ieee.org/iel5/32/35936/01703102.pdf>
> 
>     The code is here:
>     https://github.com/UnixJunkie/bisec-tree
>     <https://github.com/UnixJunkie/bisec-tree>
> 
>     It might interest users of vantage point trees (minivpt, and vpt in
>     opam), kd-trees and such.
>     I think bst should be faster than vpt in most use cases.
> 
>     It should appear in opam shortly.
> 
>     Regards,
>     Francois.
> 
> 
>     --
>     Caml-list mailing list.  Subscription management and archives:
>     https://sympa.inria.fr/sympa/arc/caml-list
>     <https://sympa.inria.fr/sympa/arc/caml-list>
>     Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>     <http://groups.yahoo.com/group/ocaml_beginners>
>     Bug reports: http://caml.inria.fr/bin/caml-bugs
>     <http://caml.inria.fr/bin/caml-bugs>
> 

^ permalink raw reply	[flat|nested] 21+ messages in thread

end of thread, other threads:[~2018-02-08  0:46 UTC | newest]

Thread overview: 21+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-01-23 14:54 [Caml-list] Are record types generative? Oleg
2018-01-23 16:05 ` Jeremy Yallop
2018-01-23 17:39   ` Chet Murthy
2018-01-23 20:35     ` Jeremy Yallop
2018-01-23 21:36       ` Chet Murthy
2018-01-23 22:06         ` Jeremy Yallop
2018-01-23 23:14           ` Hendrik Boom
2018-01-24  1:06             ` Chet Murthy
2018-01-24  1:35             ` Francois BERENGER
2018-02-07  2:00               ` [Caml-list] [ANN] first release of bst: a bisector tree implementation Francois BERENGER
2018-02-07 12:40                 ` Ivan Gotovchits
2018-02-08  0:46                   ` Francois BERENGER
2018-01-24  1:56             ` [Caml-list] Are record types generative? Yawar Amin
2018-01-25 10:49               ` Matej Košík
2018-01-25 13:39                 ` Simon Cruanes
2018-01-25 16:24                 ` Yawar Amin
2018-01-24  1:05           ` Chet Murthy
2018-01-24  8:43             ` Jacques Garrigue
2018-02-02 23:07               ` Toby Kelsey
2018-02-02 23:23                 ` Evgeny Roubinchtein
2018-02-04  1:27                 ` Jacques Garrigue

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).