Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005242OCamlOCaml generalpublic2011-03-27 01:182013-08-31 12:43
ReporterSpiceGuid 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionno change required 
PlatformOSOS Version
Product Version3.11.0 
Target VersionFixed in Version3.12.0 
Summary0005242: Non-regular recursive type leads to loss of generality
DescriptionIt seems to me the compiler assumes a recursive type to be regular even when told otherwise. The consequence is restricted generality, even when full generality is explicited.


type ('a, 'b) bijective_map =
  | Nil
  | Cons of 'a * 'b * ('b, 'a) bijective_map

let rec connected : ('a -> 'b -> bool) -> ('a, 'b) bijective_map -> bool =
  fun r -> function
  | Nil -> false
  | Cons(a,b,l) -> r a b or connected (fun x y -> r y x) l;;
val connected : ('a -> 'a -> bool) -> ('a, 'a) bijective_map -> bool = <fun>
Additional InformationUntested with 3.12.0
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005851)
garrigue (manager)
2011-03-28 03:35

There is a misunderstanding here.
The problem is not with the type definition, which does not have to be
regular for datatypes (only type abbreviations are restricted).
The problem is just that your expected type requires polymorphic
recursion, which is known to be undecidable.
Moreover your type annotation is misleading, since in ocaml type variables
appearing in annotations may be freely instantiated by the typechecker.
Since 3.12, polymorphic recursion is allowed, using a new form of type
annotation, which makes polymorphism requirements explicit.
The following code will give you the expected type.

let rec connected : 'a 'b. ('a -> 'b -> bool) -> ('a, 'b) bijective_map -> bool
=
 fun r -> function
 | Nil -> false
 | Cons(a,b,l) -> r a b or connected (fun x y -> r y x) l;;

- Issue History
Date Modified Username Field Change
2011-03-27 01:18 SpiceGuid New Issue
2011-03-28 03:35 garrigue Note Added: 0005851
2011-03-28 03:35 garrigue Status new => resolved
2011-03-28 03:35 garrigue Fixed in Version => 3.12.0
2011-03-28 03:35 garrigue Resolution open => no change required
2011-03-28 03:35 garrigue Assigned To => garrigue
2013-08-31 12:43 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker