=Paper=
{{Paper
|id=Vol-2403/paper5
|storemode=property
|title=Simple-typed Functional Language Modeled by
Category Theory
|pdfUrl=https://ceur-ws.org/Vol-2403/paper5.pdf
|volume=Vol-2403
|authors=Ján Perháč,Zuzana Bilanová,Gabriela Havrilčáková
|dblpUrl=https://dblp.org/rec/conf/icteri/PerhacBH19
}}
==Simple-typed Functional Language Modeled by
Category Theory==
https://ceur-ws.org/Vol-2403/paper5.pdf
Simple-typed Functional Language Modeled by
Category Theory
Ján Perháč1[0000−0001−6347−2409] , Zuzana Bilanová1[0000−0002−0128−5111] , and
Gabriela Havrilčáková2[0000−0002−3788−2217]
1
Department of Computers and Informatics, Faculty of Electrical Engineering and
Informatics, Technical University of Košice, Letná 9 042 00 Košice, Slovak Republic
{jan.perhac,zuzana.bilanova}@tuke.sk
2
gabriela.havrilcakova@student.tuke.sk
Abstract. In this paper we present the simply-typed Lambda calculus
extended by typed arithmetic expressions, Boolean values, derived forms,
and reference types. We briefly present its syntax and semantics. Based
on that we construct a model of this language using category theory.
Keywords: Category theory · Simply-typed Lambda calculus · Type
theory.
1 Introduction
The simply-typed Lambda calculus is considered to be the simplest functional
programming language. It was introduced by the Alonzo Church and Stephen
Kleen [1]. In our work, we use a language extended by typed arithmetic ex-
pressions, Boolean values, derived forms, and reference types. The goal of this
paper is to unify the individual extensions of simply-typed Lambda calculus to
one syntax, one many-typed signature, and one algebraic specification. Based on
that, we construct its corresponding model by category theory.
In our previous research, we have worked with type theory and linear logic [2]
[3] [4] where we have published our logical extensions of it. We have implemented
our extensions into teaching of type theory course in master level with interactive
web portal [5]. Our portal also include questionnaires for students. Based on that
we are trying to improve a course.
2 Simply Typed λ-calculus and T-NBL Definition
λ-calculus with The typed Number Boolean Language (T-NBL) is the base lan-
guage of this paper. As the basic sets of typed expressions of the λ-calculus are
considered the sets of natural numbers Nat and boolean values Bool [6], [7].
T ::= Bool | Nat (1)
Definition of simple typed λ-calculus with functional-type and with typed Num-
ber Boolean Language (T-NBL) is composed of semantics and syntax [8] with
the following syntax:
t ::= x | λx : T.t | t t | (t)| true | false | if t then t else t | 0
(2)
| succ t | pred t | iszero t.
The first four alternatives of the BNF production rule (2) belong to λ-calculus
and the others to T-NBL. Signature is define by applying the syntax of operations
and types. It is composed of pairs of sets [9]:
Σ = (T , F) (3)
– T = {Bool, Nat, T } represents a finite set of the names of basic types.
– F = {x, abs, app, true, false, if, 0, succ, pred, iszero} represents a finite
set of the specification of operations.
Signature has a pattern ΣT −N BL + λk and the following form:
ΣT −N BL + λk = (
T = {Bool, N at, T } ,
FT −N BL + λK = {
true, f alse :→ Bool,
0 :→ N at,
succ : N at → N at,
(4)
pred : N at → N at,
iszero : N at → Bool,
if : Bool, T, T → T,
x :→ T,
abs : T → T,
app : (T → T ), T → T, })
Model of algebraic specification is characterized by [10]:
1. Type assignment - to every type name T ∈ T from signature Σ is assigned
the appropriate type representation J T K,
2. Real operation assignment - to every specification of operation:
f : T1 , . . . , Tn → T0 (5)
is assigned a real appropriate operation:
Jf K : JT1 K × . . . × JTn K → J T0 K. (6)
Categorical model is created in the way that, to every name of basic types (Nat
or Bool) is assigned a set of real types (N or B) and also to the operation
specification, for example, to the pred is assigned a real operation JpredK. Real
operation works with semantic domens, on which is arity defined by cartesian
product.
Categorical model consists of objects and morphisms. Objects are considered
as semantical domens N, B, final object 0, and the initial object {*}. Morphisms
are composed of operations as follows:
– the morphisms of the T-NBL language:
• Jtrue/falseK : {*} → B defines the constants true or false.
• J0K : {*} → N defines the constant 0.
• Operations successor and predecessor are represented in the model as
Jsucc, predK : N → N. (7)
• Operation iszero is used for verification of zero value, is represented as
JiszeroK : N → B. (8)
• The conditional operation if is represented as morphism
JifK : B × (B + N) × (B + N) → B + N. (9)
– the morphisms of the λ-calculus:
• JxK : {*} → B + N morphism for expression of variable.
• JabsK : (B + N) → (B + N) morphism for expression of abstraction.
• JappK : (B + N)(B + N) × (B + N) → (B + N) morphism for expression
of application.
Model contains coprojections κ1 , κ2 and projections π1 , π2 , ϕ1 , ϕ2 , ϕ3 .
The figure 1 shows categorical model of the T-NBL (purple color) with the
λ-calculus (orange color).
3 Derived Forms Definition
Some of the programming languages have side effects, for that reason derived
forms are used [11]. Derived forms ensures, that abbreviations are established to
λ-terms, determines the evaluation approach of λ-terms, simplifying the writing
and making the code more transparent. Every derived shape can be determined
with basic forms of λ-calculus, that are sequencing, wildcards, ascription and let
binding. We add a singleton set to basic sets of typed expressions on derived
forms [10].
T ::= . . . | Unit (10)
Syntax is extended by these alternatives [8]:
t ::= . . . | (λx : Unit.t)t | (λ− : T.x)t | t as T | (λx : T.t), (11)
where the first alternative is sequence (seq), the second is wildcards (wild), the
third is ascription (asc) and the last one represents let binding (let).
Signature of derived forms consists of following:
– T = {Bool, Nat, Unit, T },
– F = {seq, wild, asc, let}.
Fig. 1. Categorical model of T-NBL and simply typed λ-calculus
And its form is:
ΣDS = (
T = {Bool, N at, U nit, T } ,
FDS = {
seq :→ U nit, T → T, (12)
wild : T → T,
asc :→ T,
let : T, T → T })
Categorical model of derived forms consists of objects, with these semantic
domens N, B, U, final object 0, and initial object {*}. Morphisms consists of
operations of derived forms as follows:
– Operation sequence is represented as morphism JseqK : (U×(B + N + U)) →
B + N + U.
– Wildcards are defined as JwildK : B + N + U → B + N + U.
– Ascription represents morphism JascK : {∗} → B + N + U,
– Let binding is JletK : ((B + N + U) × (B + N + U)) → B + N + U.
Model contains coprojections κ1 , κ2 , κ3 and projections π1 , π2 , ϕ1 , ϕ2 .
Corresponding categorical model of derived forms is depicted in the figure 2.
Fig. 2. Categorical model of derived forms
4 Reference Type Definition
In the previous sections we have mentioned just pure elements, but most pro-
gramming languages contains also inpure elements. That is the reason for some
of the side effects, and for that referentions are used. Referention determines a
value, that contains an adress of another value. Reference types are types, that
use just as much memory, as much is needed for the calculation. The basic op-
erations of reference types are alloc, dereference and assign. We add a reference
type to the basic sets of typed expressions [12], [13].
T ::= . . . | Ref (13)
Syntax is extended by these alternatives [8]:
t ::= . . . | ref t | !t | t := t, (14)
where the first alternative is alloc (ref), the second is dereference (!) and the last
one represents assign (:=).
Signature of reference types consists of:
– T = {Bool, Nat, Unit, Ref, T },
– F = {ref, !, :=}.
And has a form:
ΣRef = (
T = {Bool, N at, U nit, T } ,
FREF = {
(15)
ref : T → Ref T,
! : Ref T → T,
:= : (Ref T T ) → U nit, })
Categorical model of reference types is composed of objects [14], [15], where
belong these semantic domens N, B, R, U, final object 0, and beginning object
{*}. Morphisms contains following operations:
– alloc JrefK : (B + N + R + U) → R × (B + N + R + U),
– dereference J!K : R × (B + N + R + U) → B + N + R + U,
– assign J:=K : (B + N + R + U) × (R × (B + N + R + U)) → U.
Model contains coprojections κ1 , κ2 , κ3 , κ4 and projections π1 , π2 , ϕ1 , ϕ2 . The
corresponding categorical model of reference type is depicted in the figure 3.
Fig. 3. Categorical model of reference type
5 Simply Typed λ-calculus Extended by T-NBL, Derived
Forms and Reference Type
In this paper, we introduce the simply typed λ-calculus extended by T-NBL,
derived forms and reference type.
Basic sets of typed expressions are as follows:
T ::= Bool | Nat| Ref| Unit. (16)
The syntax of our language is expressed by the following BNF production rule:
t ::= true | false | if t then t else t | 0 | succ t | pred t | iszero t | (t)
| x | λx : T. t | t t |
| ref t | !t | t := t |
| (λx : Unit.t)t | (λ− : T.x)t | t as T | (λx : T.t).
(17)
Signature of extended simply typed λ-calculus contains:
– T = {Bool, Nat, Unit, Ref, T },
– F = {union of sets FT −N BL , FλK , FREF a FDS }.
Where:
• FT −N BL = {true, false, 0, succ, pred, iszero, if},
• FλK = {x, abs, app},
• FREF = {ref, !, :=},
• FOT = {seq, wild, asc, let}.
Signature has a form:
Σλ+T N BL+OT +Ref = (
T = {Bool, N at, U nit, T } ,
F ={
true, f alse :→ Bool,
0 :→ N at,
succ : N at → N at,
pred : N at → N at,
iszero : N at → Bool,
if : Bool, T, T → T,
x : → T, (18)
abs : T → T,
app : (T → T ), T → T,
ref : T → Ref T,
! : Ref T → T,
:= : (Ref T T ) → U nit,
seq : U nit, T → T,
wild : T → T,
asc :→ T,
let : T, T → T })
The categorical model of typed λ-calculus extended by T-NBL, reference
and derived forms was created by merging of the categorical models from past
sections. It also contains following
– coprojections κ1 , κ2 , κ3 , κ4 , and
– projections π1 , π2 , π3 , ϕ1 , ϕ2 , β1 , β2 , γ1 , γ2 , δ1 , δ2 , ε1 , ε2 .
Categorical model is depicted in the next figure 4, where the separated extensions
are represented by different colors. Purple is for the extension of T-NBL, orange
stands for λ-calculus, green is for reference and blue represents the extension of
derived forms.
Fig. 4. Categorical model of extended λ-calculus
6 Conclusions
In this paper, we have introduced the simply typed λ-calculus extended by T-
NBL, derived forms, and reference types. The main result is a unified syntax,
signature, algebraic model, and categorical model of simply typed λ-calculus
extended by T-NBL, reference types, and derived forms. Final categorical model
contains all the extensions of the simply typed λ-calculus, they are separated by
different colors for better transparency of the model.
Acknowledgment
This work was supported by the following projects:
– Faculty of Electrical Engineering and Informatics, Technical University of
Košice under the contract No. FEI-2018-59: Semantic Machine of Source-
Oriented Transparent Intensional Logic.
– Slovak Research and Development Agency under the contract No. SK-AT-
2017-0012: Semantics technologies for computer science education.
References
1. A. Church, “A formulation of the simple theory of types,” The journal of symbolic
logic, vol. 5, no. 2, pp. 56–68, 1940.
2. J. Perháč and D. Mihályi, “Intrusion detection system behavior as resource-
oriented formula,” Acta Electrotechnica et Informatica, vol. 15, no. 3, pp. 9–13,
2015.
3. L. Vokorokos, E. Danková, and N. Ádám, “Task scheduling in distributed sys-
tem for photorealistic rendering,” in 2010 IEEE 8th International Symposium on
Applied Machine Intelligence and Informatics (SAMI). IEEE, 2010, pp. 43–47.
4. J. Juhár and L. Vokorokos, “Separation of concerns and concern granularity in
source code,” in 2015 IEEE 13th International Scientific Conference on Informat-
ics. IEEE, 2015, pp. 139–144.
5. D. Mihályi, M. Peniašková, J. Perháč, and J. Mihelič, “Web based questionnaires
for type theory course,” Acta Electrotechnica et Informatica, 2017, (draft).
6. D. Mihályi and V. Novitzká, Type theory. Technical University of Košice, 2015.
7. V. Novitzká and A. Verbová, “Dependent types in mathematical theory of pro-
gramming.”
8. B. C. Pierce and C. Benjamin, Types and programming languages. MIT press,
2002.
9. H. Reichel, Initial computability, algebraic specifications, and partial algebras. Ox-
ford University Press, Inc., 1987.
10. D. Mihályi, M. Lukáč, and V. Novitzká, “Categorical semantics of reference data
type,” Acta Electrotechnica et Informatica, vol. 13, no. 4, pp. 64–69, 2013.
11. P. B. Andrews, An introduction to mathematical logic and type theory. Springer
Science & Business Media, 2002, vol. 27.
12. E. Chovancová, N. Adám, A. Baláž, E. Pietriková, P. Fecil’ak, S. Šimoňák, and
M. Chovanec, “Securing distributed computer systems using an advanced sophis-
ticated hybrid honeypot technology,” Computing and Informatics, vol. 36, no. 1,
pp. 113–139, 2017.
13. V. Novitzká and D. Mihályi, “Polymorphic type theory as a base for categorical
logic,” Acta Electrotechnica et Informatica No, vol. 7, no. 1, p. 3, 2007.
14. T. Hagino, “A typed lambda calculus with categorical type constructors,” in Cat-
egory theory and computer science. Springer, 1987, pp. 140–157.
15. L. Vokorokos, A. Baláž, and M. Chovanec, “Distributed detection system of secu-
rity intrusions based on partially ordered events and patterns,” in Towards Intel-
ligent Engineering and Information Technology. Springer, 2009, pp. 389–403.