Denotational semantics of general store and polymorphism_2

2025-05-08 0 0 739.25KB 34 页 10玖币

侵权投诉

DENOTATIONAL SEMANTICS OF GENERAL STORE AND

POLYMORPHISM

JONATHAN STERLING , DANIEL GRATZER , AND LARS BIRKEDAL

Aarhus University

e-mail address: jsterling@cs.au.dk, gratzer@cs.au.dk, birkedal@cs.au.dk

Abstract.

We contribute the ﬁrst denotational semantics of polymorphic dependent

type theory extended by an equational theory for general (higher-order) reference types

and recursive types, based on a combination of guarded recursion and impredicative

polymorphism; because our model is based on recursively deﬁned semantic worlds, it is

compatible with polymorphism and relational reasoning about stateful abstract datatypes.

We then extend our language with modal constructs for proof-relevant relational reasoning

based on the logical relations as types principle, in which equivalences between imperative

abstract datatypes can be established synthetically. What is new in relation to prior

typed denotational models of higher-order store is that our Kripke worlds need not be

syntactically deﬁnable, and are thus compatible with relational reasoning in the heap.

Our work combines recent advances in the operational semantics of state with the purely

denotational viewpoint of synthetic guarded domain theory.

1. Introduction

The combination of parametric polymorphism and general reference types in denotational

semantics is notoriously diﬃcult, though neither feature presents any serious diﬃculties on

its own.

(1)

Parametric polymorphism can be modelled in a complete internal category `a la Hy-

land [

Hyl88

]; for instance, the category of partial equivalence relations has “large”

products over the category of assemblies, which contains the assembly of all partial

equivalence relations.

(2)

General reference types can be modeled via a Kripke world-indexed state monad, where

the worlds assign syntactic types to locations in the heap, as in the possible worlds

model of thunk storage by Levy [Lev03, Lev02].

The two techniques described above are not easily combined: in order to support

parametric reasoning in the presence of reference types, it is necessary at a minimum for

the Kripke worlds to assign semantic types to locations rather than only syntactic types.

But a semantic type should itself be a family of (sets, predomains, etc.) indexed in Kripke

worlds; thus one attempts to solve a domain equation of that deﬁnes a preorder

of Kripke

worlds simultaneously with the category of functors [

Rey81

Ole86

] from

to the category

Creative Commons

arXiv:2210.02169v2 [cs.PL] 12 Apr 2023

2 J. STERLING, D. GRATZER, AND L. BIRKEDAL

of predomains:

W∼

=Loc *ﬁn.SemType SemType ∼

=[W,Predomain] (∗)

There are already a few problems with the “domain equation” presented above. For one,

the collection of predomains is not itself a predomain, but it could be replaced by the domain

of ﬁnitary projections of some universal domain [

CGW94

]. The more fundamental problem is

that it remains unclear how to interpret type connectives on

SemType

; for instance, Birkedal,

Støvring, and Thamsborg [

BST10

5] provide an explicit counterexample to demonstrate

that a na¨ıve interpretation of the reference type cannot coexist with recursive types in the

presence of semantic worlds.

1.1.

Step-indexing and guarded domain theory.

The diﬃculties outlined above have

been side-stepped by the introduction of step-indexing [

Ahm04

AMRV07

] and its semantic

counterpart metric/guarded domain theory [

AR87

RT92

BRS+11

], which proceed by strati-

fying recursive deﬁnitions in their ﬁnite approximations. This stratiﬁcation was axiomatized

by Birkedal et al. [

BMSS11

] in

synthetic guarded domain theory

/ SGDT via the

later

modality I

S S

which comes equipped with a point

idSI

; the standard

model of SGDT is the topos of trees S=Pr ωwhere the later modality is deﬁned like so:

(IA)n= lim

←−k<n Aknextn

Ax=k7→ x|k

In the setting of SGDT, any recursive deﬁnition has a unique ﬁxed point if its recursive

variables are guarded by an application of

. In categorical terms,

is algebraically compact

with respect to locally contractive endofunctors. Letting

be a type universe in a model

of synthetic guarded domain theory, it is easy to solve the following approximate domain

equation:

W∼

=Loc *ﬁn.ISemType SemType ∼

=[W,U]

The preorder

of Kripke worlds and the collection of semantic types

SemType

both exist

as objects of

; it is even possible to deﬁne a suitable connective

ref

SemType SemType

We may also deﬁne an indexed type of heaps

W→U

; unfortunately it is quite unclear

to deﬁne the indexed state monad for

as a connective on

SemType

. For instance, the

standard deﬁnition of the indexed state monad [

PP02

Lev04

Pow11

] runs into obvious size

problems given that SemType 6∈ Uand thus W6∈ U:

(TA)w=Qw0≥wHw0→Pw00 ≥w0Hw00 ×Aw00 (∗)

Indeed, the deﬁnition above cannot be executed in the standard model

Pr ω

when

is the Hofmann–Streicher lifting of a Grothendieck universe from

Set

. This problem is

side-stepped in operational models, where

is replaced by a set of predicates on syntactical

expressions of the programming language being modeled and Tis deﬁned by a guarded

version of weakest preconditions as in the original paper of Birkedal et al. [BMSS11]:

TAw ={u∈Val | ∀w0≥w, h ∈Hw0.wp(w0, h, u()){(w00, h0, v)7→ v∈Aw00}}

wp(w, h, e){Φ}= (e∈Val ∧Φ(w, h, e)) ∨ ∃w0, h0, e0.(h;e)7→ (h0;e0)∧Iwp(w0, h0){Φ}

Operational methods worked in

only because the set of predicates is a complete

lattice: we may compute the join and intersection of arbitrarily large families of predicates.

This observation will ultimately form the basis for our own non-operational solution; rather

than giving up on denotations, we will work in a diﬀerent model of synthetic guarded domain

theory that contains an

impredicative universe U

,i.e. one closed under universal and

DENOTATIONAL SEMANTICS OF GENERAL STORE AND POLYMORPHISM 3

(thus) existential types `a la System F; then we can deﬁne the indexed state monad as follows

without encountering size problems:

(TA)w=∀w0≥wHw0→∃w00 ≥w0Hw00 ×Aw00

This approach raises the question: does there in fact exist a model of synthetic guarded

domain theory with an impredicative universe? We answer in the aﬃrmative, constructing a

model in presheaves on a well-founded order internal to a

realizability topos

[

vO08

]. Our

model of SGDT is thus an instance of the relative-topos-theoretic generalization of synthetic

guarded domain theory introduced by Palombi and Sterling [PS23].

1.2.

This paper: impredicative guarded dependent type theory with reference

types.

Our denotational model of higher-order store was immediately suited for generaliza-

tion to dependent types; this scalability is one of many advantages our abstract category-

theoretic methods. Justiﬁed by this model, we have deﬁned Impredicative Guarded Depen-

dent Type Theory (

iGDTT

) and its extension with general reference types (

iGDTTref

)

and their equational theory.

iGDTTref

is the ﬁrst language to soundly combine “full-spectrum” dependently typed

programming and equational reasoning with both higher-order store and recursive types.

The necessity of semantics for higher-order store with dependent types is not hypothetical:

both Idris 2 and Lean 4 are dependently typed, higher-order functional programming

languages [

Bra21

DMU21

] that feature a Haskell-style

monad with general

IORef

types [

Jon01

], but until now these features have had no semantics. In fact, our investigations

have revealed a potential problem in the

monads of both Idris and Lean: as higher-order

store seems to be inherently impredicative, it may not make sense to close multiple nested

universes under the IO monad [Coq86].

Many real-world examples require one to go beyond simple equational reasoning; to

this end, we deﬁned an extension

iGDTTref

lrat

with constructs for synthetic, proof-relevant

relational reasoning for data abstraction and weak bisimulation based on the

logical re-

lations as types

(LRAT) principle of Sterling and Harper [

SH21

], which axiomatizes a

generalization of the parametricity translation of dependent type theory [BJP12, BM12].

1.3. Discussion of related work.

1.3.1. Operational semantics of higher-order store. The most thoroughly developed methods

for giving semantics to higher-order store are based on operational semantics [

Ahm04

];

accompanying the operational semantics of higher-order store is a wealth of powerful

program logics for modular reasoning about higher-order eﬀectful and even concurrent

programs based on higher-order separation logic [SB14, JKJ+18, BB18].

We are motivated to pursue denotations for three reasons. First, denotational methods

are amenable to the use of general theorems from other mathematical ﬁelds to solve diﬃcult

domain problems, whereas operational methods tend to require one to solve every problem

“by hand” without relying on standard lemmas. Secondly, a good denotational semantics tends

to simplify reasoning about programs, as the exponents of the DeepSpec project have argued

[

XZH+19

]. Finally and most profoundly, there is an emerging need to program directly with

actual spaces, as in diﬀerentiable and probabilistic programming languages [

AP19

VKS19

4 J. STERLING, D. GRATZER, AND L. BIRKEDAL

Although operational and denotational semantics are diﬀerent in both purpose and

technique, there is nonetheless a rich interplay between the two traditions. First of all,

the idea of step-indexing and its approximate equational theory lies at the heart of our

denotational semantics; second, the wealth of results in operationally based models and

program logics for higher-order store suggest several areas for future work in our denotational

semantics. For instance, it would be interesting to rebase a program logic such as Iris atop our

synthetic denotational model; likewise, several perationally based works [

ADR09

DNRB10

]

suggest many improvements to our notion of semantic world to support richer kinds of

correspondence between programs.

1.3.2. Denotational semantics of state. There is a rich tradition of denotational semantics

of state, ranging from a single reference cell [

Mog91

] to ﬁrst-order store [

PP02

] and storage

of pointers [

KLMS17

], and even higher-order store with syntactic worlds [

Lev04

]. None of

these approaches is compatible with relational reasoning for polymorphic/abstract types, as

they all rely on the semantic heap being classiﬁed by syntactically deﬁnable types.

Untyped metric semantics and approximate locations.

A somewhat diﬀerent untyped

approach to the denotational semantics of higher-order store with recursive types and

polymorphism was pioneered by Birkedal, Støvring, and Thamsborg [BST10] in which one

uses metric/guarded domain theory to deﬁne a universal domain D, and then develops a

model of System

Fref

in predicates on D. Because predicates form a complete lattice, it is

possible to interpret the state operations as we have discussed in Section 1.1. An important

aspect of this class of models is the presence of approximate locations, which op. cit. have

shown to be non-optional.1

Comparison.

Our own model resembles a synthetic version of that of Birkedal, Støvring,

and Thamsborg [

BST10

], but there are some important diﬀerences. Our model is considerably

more abstract and more general than that of op. cit.; whereas the cited work must solve

a very complex metric domain equation to construct a universal domain, we may use the

realizability topos generated by any partial combinatory algebra, and thus we do not depend

on any speciﬁc choice of universal domain. Moreover, we argue that ours is a typed model:

we depend only on the combination of guarded recursion and an impredicative universe,

and although the principle source of such structures is realizability on untyped partial

combinatory algebras [

LS02

], we do not depend on any of the details of realizability. Because

of the generality and abstractness of our model construction, scaling up to full dependent

type theory has oﬀered no resistance.

1.3.3. Higher-order store in Impredicative Hoare Type Theory. Realizability models of im-

predicative type theory have been used before to give a model of so-called Impredicative

Hoare Type Theory (

iHTT

), an extension of dependent type theory with a monadic “Hoare”

type for stateful computations with higher-order store [

SBN11

]. However, in contrast to our

monadic type in

iGDTTref

iHTT

does not support equational reasoning about compu-

tations: all elements of a Hoare type are equated and one can only reason via the types.

Moreover, the Hoare type in op. cit. only supports untyped locations with substructural

Indeed, even in our own model the presence of approximate locations can be detected using Thamsborg’s

observation on the correspondence between metric and ordinary domain theory [Tha10, Ch. 9].

DENOTATIONAL SEMANTICS OF GENERAL STORE AND POLYMORPHISM 5

reference capabilities that change as the heap evolves (the so-called “strong update”); thus

non-Hoare types are not indexed in worlds.

1.3.4. Linear dependent type theory. Another approach to the integration of state into

dependent type theory is contributed by Krishnaswami, Pradic, and Benton [

KPB15

], who

develop an adjoint linear–non-linear dependent type theory

LNLd

with a realizability model

in partial equivalence relations. Like

iHTT

, the theory of op. cit. uses capabilities for

references with strong update; unlike

iHTT

, the account of store in

LNLd

enjoys a rich

equational theory. What is missing from

LNLd

is any account of general recursion, which

normally arises from higher-order store via backpatching or Landin’s Knot; indeed,

LNLd

carefully avoids the general recursive aspects of higher-order store via linearity. One of the

main advances of our own paper over both

iHTT

and

LNLd

is to model a dependently

typed equational theory for full store with general recursion.

1.3.5. Eﬀectful dependent type theory. We have not attempted any non-trivial interaction

between computational eﬀects and the dependent type structure of our language, in contrast

to the work of P´edrot and Tabareau [

PT19

] on dependent call-by-push-value: our

iGDTTref

language can be thought of as a purely functional programming language extended with a

monad for stateful programming with Haskell-style IORefs.

1.4. Structure and contributions of this paper. Our contributions are as follows:

•

Section 2

we introduce

impredicative guarded dependent type theory

(

iGDTT

)

as a user-friendly metalanguage for the denotational semantics of languages involving

polymorphism, general reference types and recursive types. In

Section 2.4

as a case

study, we construct a simple denotational model of Monadic System

Fref

, a language with

general reference types, polymorphic types, and recursive types in

iGDTT

. Finally in

Section 2.5

we describe our Coq library for

iGDTT

in which we have formalized the

higher-order state monad and reference types.

•

Section 3

we describe

iGDTTref

, an extension of

iGDTT

with general reference

types and a monad for higher-order store.

iGDTTref

is thus a full-spectrum dependently

typed programming language with support for higher-order eﬀectful programming. To

illustrate the combination of higher-order store with dependent types, we deﬁne and

prove the correctness of an implementation of factorial deﬁned via

Landin’s knot

backpatching.

•

Section 4

we describe

iGDTTref

lrat

, an extension of

iGDTTref

with constructs for

synthetic proof-relevant relational reasoning based on the

logical relations as types

principle [

SH21

iGDTTref

lrat

can be used to succinctly exhibit bisimulations between

higher-order stateful computations and abstract data types, which we demonstrate in two

case studies involving imperative counter implementations (Sections 4.3 and 4.4).

•

Section 5

, we describe general results for constructing models of

iGDTT

and

iGDTTref

lrat

, with concrete instantiations given by a combination of realizability and

internal presheaves. The results of this section justify the consistency of

iGDTTref

lrat

as a

language for relational reasoning about higher-order stateful computations.

•In Section 6 we conclude with some reﬂections on directions for future work.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

DENOTATIONALSEMANTICSOFGENERALSTOREANDPOLYMORPHISMJONATHANSTERLING,DANIELGRATZER,ANDLARSBIRKEDALAarhusUniversitye-mailaddress:jsterling@cs.au.dk,gratzer@cs.au.dk,birkedal@cs.au.dkAbstract.Wecontributetherstdenotationalsemanticsofpolymorphicdependenttypetheoryextendedbyanequationaltheoryforgeneral(h...

展开>> 收起<<

Denotational semantics of general store and polymorphism_2.pdf

共34页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Denotational semantics of general store and polymorphism_2

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: