Polymoprhic Algebraic Theoreis- Syntax, Semantics, Translations, and Eqational Logic LICS 2013,

University of Cambridge, UK
Gunma University, JapanJune, Tulane University

Marcelo Fiore
Makoto Hamana

WhatisPolymorphism

Polymorphic types = “variable types”

have many instancesVarious Polymorphic Sytems[Girard’71, Reynolds’74]

System F
System Fω
λUML, Haskell

OO Languages
Java, C++, Scala,etc.

[Milner’75,78]

System Fc↑[Girard’72]

Polymorphic
Record Calculus[Ohori’95][Yorgey et al.’12]

Polymorphicπ-calculus

PolymorphicContracts[Guha, et al. ’07] [Belo et al.’11][Pierce, Sanngiorgi’00]

Polymorphic
Logic Programming[Shapiro’91][Hanus’91]

Polymorphic
XML[Hosoya et al.’09]⇒Unified Theory for Polymorphism⇒Mutiversal Polymoprhic Algebraic Theoreis

o f Ty p e s
System FTyeps

System Fω
Tyeps

λUTyepsPolymorphic
Record Calculus
Tyeps

ML, Haskell
Tyeps

System Fc↑

Java, C++, Scala,etc.

Tyeps

Tyeps

Polymorphic
π-calculus
Tyeps

Polymorphic
Logic Programming

Tyeps- Universe

OO Languages

Polymorphic
Contracts
Tyeps

PolymorphicXMLTyeps= collection of all types (cf. Martin-Lof Type Theory)= multiple type universes- Translation = algebra homomorphism

How to give Algebraic Theory• Signatures, terms, equations• Clones in universal algebra• Lawvere theories• (Finitary) monads• Cartesian multicategories

Polymorphic
What is an Algebraic Theory

types, contexts• Signatures, terms, equations

(Polymorphic λ-calculus)
metavariablebinding

object variable

type metavariablemeta-level subst.

Various other examples- Existential λ- Polymorphic FPC- Algebraic theory for global stateHow to Built Polymorphic Algebirac Theory
Algebraic Characterisation of
Untyped Syntax with Variable Binding[Fiore, Plotkin, Turi LICSʼ99]
with Metavariables[H. APLASʼ04]
via Σ-monoids

Polymorphic Abstract Syntax[H. FoSSaCSʼ11]
via Grothendieck Constr.

This work
Polymorphic Abstract Syntax with Metavariables

Polymorphic Algebraic Theories

initial F-algebra(Polymorphic λ-calculus)Polymorphic Case?
Esp.

type univese⇒Collect all possible dependent triples

Types depend on type variable contexts

Def.
A universe of polymorphic types
isa Σ-monoid
signature for type constructors.

Category of Discourse for Polymorphic Systems

type context

The Grothendieck Construction
gives dependent triples.

(Polymorphic λ-calculus)
type metavariablemeta-level subst.

Endofunctor for Polymorphic Syntax
signature

universe =-monoid

polynomial diagram in Cat[Moerdijk, Palmgren,Gambino,Hyland,Kock,Batanin,Weber,...]

endofunctor

General notion of models

Freepolymorphic structure
as “syntax with metavariabls”
metavariabels

Homomorphism = interpretation
Category

polymorphic strucres- homomorphisms

Anypolymorphic structure
as “semantics”▶ We may want to change a universe U
in interpretation

metavariablebindingtype metavariablemeta-level subst.

Various examples- Existential λ- Polymorphic FPC- Algebraic theory for global statePaper
Multiversal Polymorphic Algebraic Theories:
Syntax, Semantics, Translations, and Equational Logic
Proc. of Twenty-Eighth Annual ACM/IEEE Symposium on
Logic in Computer Science (LICS 2013), IEEE Press.
http://www.cs.gunma-u.ac.jp/~hamana/