Against a Universal Definition of 'Type'

Tomas Petricek

In Proceedings of Onward! Essays 2015

What is the definition of 'type'? Having a clear and precise answer to this question would avoid many misunderstandings and prevent meaningless discussions that arise from them. But having such clear and precise answer to this question would also hurt science, "hamper the growth of knowledge" and "deflect the course of investigation into narrow channels of things already understood".

In this essay, I argue that not everything we work with needs to be precisely defined. There are many definitions used by different communities, but none of them applies universally. A brief excursion into philosophy of science shows that this is not just tolerable, but necessary for progress. Philosophy also suggests how we can think about this imprecise notion of type.

Watch the talk

As far as I know, the Onward! Essays talk has not been recorded, but I did a more recent talk about the topic of the paper at Lambda Days 2016 conference organized by Erlang Solutions. You can watch my History and Philosophy of types talk below, or on Vimeo.

Paper and more information

• Download the paper (PDF)

Bibtex

If you want to cite the paper, you can use the following BibTeX information.

1: 
2: 
3: 
4: 
5: 
6: 
7: 
8: 

@inproceedings{against-types-onward15,
  author    = {Petricek, Tomas},
  title     = {Against a Universal Definition of 'Type'},
  booktitle = {Proceedings of Onward! Essays},
  series    = {Onward! 2015},
  location  = {Pittsburg, USA},
  year      = {2015}
}

If you have any comments, suggestions or related ideas, I'll be happy to hear from you! Send me an email at tomas@tomasp.net or get in touch via Twitter at @tomaspetricek.