On the sister thread
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-July/msg00028.html
Henri mentions finite_UNIV.
Henri refers to finite_UNIV in HOL/Finite_Set, you seem to talk about
finite_UNIV from HOL/Library/Cardinality.
Trying to reproduce the observed effects with Isabelle2012 vs.
Isabelle/3155cee13c49 from today reveals a difference wrt. Phantom('a).
The latter was introduced in Isabelle/f0ecc1550998 with an almost vacous
log entry, and no coverage in NEWS nor CONTRIBUTORS.
I planned to cover the whole business of phantom type and the type classes
finite_UNIV and card_UNIV once I have finished moving FinFuns from the AFP to
HOL/Library.
What is its purpose? Where is it documented?
The first hit in Google when you search for "phantom type" tells you what a
phantom type is.
"A phantom type is a type whose type parameter do not all appear on the
right-hand side of it's defintion."
[http://www.haskell.org/haskellwiki/Phantom_type]
As can be seen from the usage of Phantom('a) in Cardinality (e97369f20c30 and
3d9c1ddb9f47) and the commit message in e97369f20c30, phantom types can be used
to make a type parameter appear in a constant's type. Typically in Isabelle,
such constants take an additional argument 'a itself for that purpose, but this
generates less efficient code than boxing values in phantom types of which the
ML/Haskell compiler gets rid again.
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: [email protected]
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
