Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adding explicit recursive typing support #5923

Closed
vicuna opened this issue Feb 16, 2013 · 8 comments
Closed

Adding explicit recursive typing support #5923

vicuna opened this issue Feb 16, 2013 · 8 comments

Comments

@vicuna
Copy link

vicuna commented Feb 16, 2013

Original bug ID: 5923
Reporter: @bobzhang
Assigned to: @gasche
Status: closed (set by @xavierleroy on 2015-12-11T18:18:29Z)
Resolution: not a bug
Priority: normal
Severity: feature
Category: typing

Bug description

the 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

@vicuna
Copy link
Author

vicuna commented Feb 16, 2013

Comment author: @gasche

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

@vicuna
Copy link
Author

vicuna commented Feb 16, 2013

Comment author: @bobzhang

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

@vicuna
Copy link
Author

vicuna commented Feb 16, 2013

Comment author: @bobzhang

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

@vicuna
Copy link
Author

vicuna commented Feb 16, 2013

Comment author: @bobzhang

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

@vicuna
Copy link
Author

vicuna commented Feb 16, 2013

Comment author: @sliquister

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 ]

@vicuna
Copy link
Author

vicuna commented Feb 16, 2013

Comment author: @bobzhang

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

@vicuna
Copy link
Author

vicuna commented Feb 16, 2013

Comment author: @gasche

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.

@vicuna
Copy link
Author

vicuna commented Feb 16, 2013

Comment author: @bobzhang

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants