Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005923OCamltypingpublic2013-02-16 16:002015-12-11 19:18
Assigned Togasche 
PrioritynormalSeverityfeatureReproducibilityhave not tried
StatusclosedResolutionno change required 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0005923: Adding explicit recursive typing support
Descriptionthe structual typing by polymorphic variants have more support for polymorphism than Algebraic Data Types. It can be improved a bit with explicit recursive typing support.

Suppose we have three types
type a_and_b = [ `AB of (int * a_and_b)]
type a = [`AB of (int *a) | `A]
type b = [`AB of (int *b) | `B]

With explicit recursive types, it can be written as
type a_and_b = [`AB of (int * self)]
type a = [ a_and_b | `A]
type b = [a_and_b | `B]

For both, the semantics are exactly the same, except that the second solution saves a lot of typing when the types are large. Thanks

TagsNo tags attached.
Attached Files

- Relationships

-  Notes
gasche (developer)
2013-02-16 17:55

Honestly, this looks like a terrible idea to me. It is not even clear why this is needed (couldn't you choose a shorter name in the first place, or use a short type synonym?), but much more importantly it breaks the regularity of the language by introducing new ways to do the same things that feels more like kludge than important ideas.

Any option you add to the language has a cost for tools, documentation, or simply cognitive load of programmers reading the code. This one feature is clearly not worth the cost.

Besides, it breaks some arguably nice aspects of the design of the language, which is careful not to introduce identifiers implicitly. Heck, even in objects "self" is a user-bound explicit identifier. If we resisted the temptation to have an implicit self there, surely we should stick to this decision here.

(I understand that this is a result of your experimentation with polymorphic variant to describe large ASTs, and that you may therefore have credible but large use-cases for this feature. However, if for every problem an user had we accepted to add a new feature to the language, instead of having the user find an actual solution, we would be in a terrible, terrible mess right now, and that's not where we want to be in ten years either.)
hongboz (developer)
2013-02-16 18:15

@gasche, would you elaborate a bit why this is a terrible idea? what do you mean by introducing a shorter name in the first place?
hongboz (developer)
2013-02-16 18:20

The case is that type a_and_b is a large recursive type, currently the best we can do is copy paste all branches of a_and_b into both a and b.
This feature, to my knowledge, is mostly a syntax sugar, would you elaborate a bit why this would result in an ugly design? Thanks
hongboz (developer)
2013-02-16 18:25

choosing `self' as a keyword may not be a good idea, but we could pick some existing keywords here, for example, 'rec'.
type a_and_b = [`AB of (int * rec)]
sliquister (reporter)
2013-02-16 23:09

What about:

$ ocaml
        OCaml version 4.01.0+dev10-2012-10-16

# type 'self a_and_b = [ `AB of (int * 'self) ];;
type 'self a_and_b = [ `AB of int * 'self ]
# type a = [ a a_and_b | `A ];;
type a = [ `A | `AB of int * a ]
# type b = [ b a_and_b | `B ];;
type b = [ `AB of int * b | `B ]
hongboz (developer)
2013-02-16 23:37

@sliquister This is pretty neat, I did think about it, but I did not try it yet, introduces a type variable would complicate our Ast too much(several mutual recursive data type would introduce too many type variables)

Since in OCaml, both objects and variants support structual typing, objects provides a self for recursive objects, I think it's reasonable to support such feature in variants as well.
gasche (developer)
2013-02-16 23:51

A type such as you suggest would make the type system "impure" in the sense of breaking referential transparency: `a_and_b` could not be understood as a type expression in itself, as its meaning is different in the two later types

  type a = [ a_and_b | `A]
  type b = [ a_and_b | `B]

Impurity is debatable at the term level, it would be horrible at the type level. If you want recursion, represent it explicitly as in sliquister helpful example.
hongboz (developer)
2013-02-17 00:02

Well, we did not rely on this feature fundamentally. IMHO, this is discuss-able

- Issue History
Date Modified Username Field Change
2013-02-16 16:00 hongboz New Issue
2013-02-16 17:55 gasche Note Added: 0008845
2013-02-16 18:15 hongboz Note Added: 0008846
2013-02-16 18:20 hongboz Note Added: 0008847
2013-02-16 18:25 hongboz Note Added: 0008848
2013-02-16 23:09 sliquister Note Added: 0008849
2013-02-16 23:37 hongboz Note Added: 0008850
2013-02-16 23:51 gasche Note Added: 0008851
2013-02-16 23:51 gasche Status new => resolved
2013-02-16 23:51 gasche Resolution open => no change required
2013-02-16 23:51 gasche Assigned To => gasche
2013-02-17 00:02 hongboz Note Added: 0008852
2015-12-11 19:18 xleroy Status resolved => closed
2017-02-23 16:45 doligez Category OCaml typing => typing

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker