[TYPES] When types appeared in programming languages

[Simone Martini]

Dear Patrick,

Joe Goguen’s paper is a fine piece of work, which observes and classifies the use (and role) of types in PL from a semantical perspective (types as “sets”, as “algebras” and “theories”).

Once could be tempted to say that these three “types” correspond to what I call the "technical concept”, the "general abstraction mechanism” and the types from mathematical logic. 
But I believe this would be a post festam reconstruction. 
Until the turn from the ’60s to the ’70s (and thus papers by Goguen, Hoare, and of course Liskov) there are no real “types as algebras” around. 

Of course, the “types as theories” are the “types of logic” (at least one particular way to understand them), independent from the Curry-Howard isomorphism, but they arrive on the scene in the 80s… 

Best regards and thank you for sharing with us your observations.

-s.




> On 16 Oct 2015, at 13:48, PATRICK BROWNE <patrick.browne at dit.ie> wrote:
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Simone,
> I enjoyed your review of types. Have you looked at Joseph Goguen's paper
> Type as Theories[1].
> He presents three descriptions of types: 1)as sets, 2)as algebras, 3)as
> theories.
> I believe that algebraic languages like CafeOBJ and Maude support all three
> approach to types.
> Types as sets: Using *sorts*, which can be arrange in a lattice of sorts.
> Types as algebras: Tight modules with carrier set, and concrete operations
> using initial semantics
> Types as theories: Loose modules representing theories with axioms stating
> properties e.g. partial order, monoid.
>                   Types are logical theories, presented by axioms, whose
> properties can be explored by logical deduction.
> Regards,
> Pat
> [1]
> http://www.google.ie/url?sa=t&rct=j&q=&esrc=s&source=web&cd=4&cad=rja&uact=8&ved=0CDQQFjADahUKEwib3eGM1MbIAhXC6xQKHcsLA4A&url=http%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fdownload%3Fdoi%3D10.1.1.16.2241%26rep%3Drep1%26type%3Dps&usg=AFQjCNGjxJGhAumTd7mV0iNovz3eKUco3g&bvm=bv.105039540,d.d24
> 
> On 14 October 2015 at 10:26, Simone Martini <simone.martini at unibo.it> wrote:
> 
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
>> ]
>> 
>> Last year, there has been a thread on this mailing list on the role (and
>> concept) of types in programming languages, started by this msg of Vladimir
>> Voevodsky:
>>        http://lists.seas.upenn.edu/pipermail/types-list/2014/001745.html
>> 
>> Stimulated from that thread (which showed that there was little consensus
>> on when types appeared, and with which meaning), I wrote a little essay,
>> suggesting that the emergence of the concept of type in computer science is
>> relatively independent from the logical tradition, until the Curry-Howard
>> isomorphism will make an explicit bridge between them.
>> 
>> I presented the paper last week at History and Philosophy of Computing
>> 2015, in Pisa.
>> 
>>        http://arxiv.org/abs/1510.03726
>> 
>> Comments, remarks, and especially critiques would be much welcomed from
>> the members of this list.
>> 
>> Best,
>> -s.
>> ---------------------------------------------------
>> Simone Martini
>> Universita' di Bologna
>> Dip. di Informatica - Scienza e Ingegneria
>> Italy
>> 
>> www.cs.unibo.it/~martini
>> 
> 
> -- 
> 
> 
> This email originated from DIT. If you received this email in error, please 
> delete it from your system. Please note that if you are not the named 
> addressee, disclosing, copying, distributing or taking any action based on 
> the contents of this email or attachments is prohibited. www.dit.ie
> 
> Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí 
> earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an 
> seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon 
> dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa 
> ríomhphost nó sna hiatáin seo. www.dit.ie
> 
> Tá ITBÁC ag aistriú go Gráinseach Ghormáin – DIT is on the move to 
> Grangegorman <http://www.dit.ie/grangegorman>