Ssreflect Users Discussion List

[Enrico Tassi <>]

On Wed, Dec 06, 2017 at 09:59:11PM +0000, Arthur Azevedo de Amorim wrote:
> Phantom types are used in several places of mathcomp to infer canonical
> structures. Is there any reason for preferring, e.g.
> 
>     Record my_type (T : eqType) := MyType {value : T; _ : some_pred value}.
>     Definition my_type_of (T : eqType) of phant T := my_type T.
> 
> over
> 
>     Record my_type (T : eqType) (p : phant T) := MyType (value : T; _ :
> some_pred value).

I don't know if it is the main reason, but I've always had the feeling
that "phantom types" are used as a device to ease the construction of
objects, they are not morally part of the object you are defining.
A bit like smart constructors in functional programming languages.

Best,
-- 
Enrico Tassi