[TYPES] Do "phantom types" mean types like ('a, 'n)sized_list as a whole, or dummy parameters like 'n itself?

[Derek Dreyer]

Hi, Eijiro.  I believe that the phrase "phantom types" is mostly used
in the literature to refer to the entire *technique* of programming
with phantom types, not to the actual types themselves.  Used in that
way, it is unambiguous.

I would agree with your intuition and assessment that when it comes to
the types themselves, it is the dummy type variables (like 'n in your
example) that are phantom-like, not the type constructors that are
parameterized by them.  But on the other hand, I can imagine practical
reasons for the alternative (and apparently more common) usage.  For
example, if phantom types refer to the type constructors, one can say,
"And now let's define some phantom types," whereas if phantom types
refer to the dummy type variables one is forced to more awkwardly say,
"And now let's define some types that are parameterized by phantom
types."

Best regards,
Derek


On Sat, Jan 11, 2014 at 10:02 AM, Eijiro Sumii <eijiro.sumii at gmail.com> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear Types people,
>
> I am (again) asking a question about terminology: recently, a student
> of mine and I have been developing a library extensively using
> so-called phantom types.  As far as we understand, phantoms types are
> concerned with polymorphic data types whose type parameter does not
> appear in the r.h.s. of the definition, e.g. (in OCaml syntax),
>
>   type ('a, 'n) sized_list = 'a list
>     (* should be made abstract by module signature *)
>
> where
>
>   type zero (* no constructor *)
>   type 'n succ (* no constructor *)
>   let nil : ('a, zero) sized_list = []
>   let cons ((a : 'a), (d : ('a, 'n) sized_list))
>     : ('a, 'n succ) sized_list = a :: d
>   let car (x : ('a, 'n succ) sized_list)
>     : 'a = List.hd x
>   let cdr (x : ('a, 'n succ) sized_list)
>     : ('a, 'n) sized_list = List.tl x
>
> (this example is for pedagogy only).
>
> My question is: do phantom types mean types like ('a,'n)sized_list as
> a whole, or dummy parameters like 'n itself?  The majority of the
> literature (and Web pages) means the former, while some seem to mean
> the latter.
>
> For me, the latter (the minority) seems to be more "logical" since
> there is no constructor for the types substituted with 'n (hence the
> terminology "phantom"), while ('a,'n)sized_list itself *does* have
> flesh and blood (i.e., values).  Does anybody know any historical
> reason for the former (the major) terminology?
>
> N.B.  Yes, the types zero and 'n succ are like type void (in the sense
> of type theory, not C), but they are distinguished from each other by
> the names.
>
> Best regards,
>
>         Eijiro