[isabelle-dev] Type arguments in datatype declarations

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Sep 27 13:37:36 CEST 2010

The following datatype specification succeeds as expected

datatype ('a, 'b) foo = Nihil | Bar "('a, 'b) bar"
  and ('a, 'b) bar = Foo "('a, 'b) foo"

whereas the following logically equivalent, but differently written
specification fails with a low-level exception in size.ML:

datatype ('a, 'b) foo = Nihil | Bar "('b, 'a) bar"
  and ('b, 'a) bar = Foo "('a, 'b) foo"

I have always assumed gracefully that for mutual datatype specifications
the names of arguments must be strictly the same, and many recent
extensions to the datatype package also do.  Have specifications like
the second ever been intended to succeed?  If yes, the issue could be
solved by consolidating specifications silently before processing.  If
no, a user-level error message should be reported.

My personal preference is the second, but there might be different opinions.




PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100927/b26b0298/attachment.sig>

More information about the isabelle-dev mailing list