[isabelle-dev] Fwd: [isabelle] Pending sort hypotheses

[Andreas Lochbihler]

> 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: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft