0005242: Non-regular recursive type leads to loss of generality - MantisBT

Mantis Bug Tracker

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0005242

OCaml

OCaml general

public

2011-03-27 01:18

2011-03-28 03:35

Reporter

SpiceGuid

Assigned To

garrigue

Priority

normal

Severity

minor

Reproducibility

always

Status

resolved

Resolution

no change required

Platform

OS

OS Version

Product Version

3.11.0

Target Version

Fixed in Version

3.12.0

Summary

0005242: Non-regular recursive type leads to loss of generality

Description

It 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 Information

Untested with 3.12.0

Tags

No tags attached.

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

Copyright © 2000 - 2011 MantisBT Group