A family of syntactic logical relations for the semantics of Haskell-like languages

Patricia Johann, Johann Voigtlander

Research output: Contribution to journalArticle

5 Citations (Scopus)

Abstract

Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming language features have been introduced in recent years. Unfortunately, the calculi studied are typically idealized, and the results obtained for them offer only partial insight into the impact of such features on observational behavior in implemented languages. In this paper, we show how to bring reasoning via logical relations closer to bear on real languages by deriving results that are more pertinent to an intermediate language for the (mostly) lazy functional language Haskell like GHC Core. To provide a more fine-grained analysis of program behavior than is possible by reasoning about program equivalence alone, we work with an abstract notion of relating observational behavior of computations which has among its specializations both observational equivalence and observational approximation. We take selective strictness into account, and we consider the impact of different kinds of computational failure, e.g., divergence versus failed pattern matching, because such distinctions are significant in practice. Once distinguished, the relative definedness of different failure causes needs to be considered, because different orders here induce different observational relations on programs (including the choice between equivalence and approximation). Our main contribution is the construction of an entire family of logical relations, parameterized over a definedness order on failure causes, each member of which characterizes the corresponding observational relation. Although we deal with properties very much tied to types, we base our results on a type-erasing semantics since this is more faithful to actual implementations.
LanguageEnglish
Pages341-368
Number of pages28
JournalInformation and Computation
Volume207
Issue number2
DOIs
Publication statusPublished - Feb 2009

Fingerprint

Haskell
Pattern matching
Syntactics
Polymorphism
Computer programming languages
Semantics
Reasoning
Equivalence
Calculus
Pattern Matching
Approximation
Specialization
Faithful
Programming Languages
Family
Syntax
Language
Divergence
Entire
Partial

Keywords

  • logical relations
  • reasoning
  • language programs
  • parametric polymorphism
  • observational behavior
  • polymorphic calculi

Cite this

Johann, Patricia ; Voigtlander, Johann. / A family of syntactic logical relations for the semantics of Haskell-like languages. In: Information and Computation. 2009 ; Vol. 207, No. 2. pp. 341-368.
@article{73d6b5cefc51463bb065d183a103a115,
title = "A family of syntactic logical relations for the semantics of Haskell-like languages",
abstract = "Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming language features have been introduced in recent years. Unfortunately, the calculi studied are typically idealized, and the results obtained for them offer only partial insight into the impact of such features on observational behavior in implemented languages. In this paper, we show how to bring reasoning via logical relations closer to bear on real languages by deriving results that are more pertinent to an intermediate language for the (mostly) lazy functional language Haskell like GHC Core. To provide a more fine-grained analysis of program behavior than is possible by reasoning about program equivalence alone, we work with an abstract notion of relating observational behavior of computations which has among its specializations both observational equivalence and observational approximation. We take selective strictness into account, and we consider the impact of different kinds of computational failure, e.g., divergence versus failed pattern matching, because such distinctions are significant in practice. Once distinguished, the relative definedness of different failure causes needs to be considered, because different orders here induce different observational relations on programs (including the choice between equivalence and approximation). Our main contribution is the construction of an entire family of logical relations, parameterized over a definedness order on failure causes, each member of which characterizes the corresponding observational relation. Although we deal with properties very much tied to types, we base our results on a type-erasing semantics since this is more faithful to actual implementations.",
keywords = "logical relations, reasoning, language programs, parametric polymorphism, observational behavior, polymorphic calculi",
author = "Patricia Johann and Johann Voigtlander",
year = "2009",
month = "2",
doi = "10.1016/j.ic.2007.11.009",
language = "English",
volume = "207",
pages = "341--368",
journal = "Information and Computation",
issn = "0890-5401",
number = "2",

}

A family of syntactic logical relations for the semantics of Haskell-like languages. / Johann, Patricia; Voigtlander, Johann.

In: Information and Computation, Vol. 207, No. 2, 02.2009, p. 341-368.

Research output: Contribution to journalArticle

TY - JOUR

T1 - A family of syntactic logical relations for the semantics of Haskell-like languages

AU - Johann, Patricia

AU - Voigtlander, Johann

PY - 2009/2

Y1 - 2009/2

N2 - Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming language features have been introduced in recent years. Unfortunately, the calculi studied are typically idealized, and the results obtained for them offer only partial insight into the impact of such features on observational behavior in implemented languages. In this paper, we show how to bring reasoning via logical relations closer to bear on real languages by deriving results that are more pertinent to an intermediate language for the (mostly) lazy functional language Haskell like GHC Core. To provide a more fine-grained analysis of program behavior than is possible by reasoning about program equivalence alone, we work with an abstract notion of relating observational behavior of computations which has among its specializations both observational equivalence and observational approximation. We take selective strictness into account, and we consider the impact of different kinds of computational failure, e.g., divergence versus failed pattern matching, because such distinctions are significant in practice. Once distinguished, the relative definedness of different failure causes needs to be considered, because different orders here induce different observational relations on programs (including the choice between equivalence and approximation). Our main contribution is the construction of an entire family of logical relations, parameterized over a definedness order on failure causes, each member of which characterizes the corresponding observational relation. Although we deal with properties very much tied to types, we base our results on a type-erasing semantics since this is more faithful to actual implementations.

AB - Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming language features have been introduced in recent years. Unfortunately, the calculi studied are typically idealized, and the results obtained for them offer only partial insight into the impact of such features on observational behavior in implemented languages. In this paper, we show how to bring reasoning via logical relations closer to bear on real languages by deriving results that are more pertinent to an intermediate language for the (mostly) lazy functional language Haskell like GHC Core. To provide a more fine-grained analysis of program behavior than is possible by reasoning about program equivalence alone, we work with an abstract notion of relating observational behavior of computations which has among its specializations both observational equivalence and observational approximation. We take selective strictness into account, and we consider the impact of different kinds of computational failure, e.g., divergence versus failed pattern matching, because such distinctions are significant in practice. Once distinguished, the relative definedness of different failure causes needs to be considered, because different orders here induce different observational relations on programs (including the choice between equivalence and approximation). Our main contribution is the construction of an entire family of logical relations, parameterized over a definedness order on failure causes, each member of which characterizes the corresponding observational relation. Although we deal with properties very much tied to types, we base our results on a type-erasing semantics since this is more faithful to actual implementations.

KW - logical relations

KW - reasoning

KW - language programs

KW - parametric polymorphism

KW - observational behavior

KW - polymorphic calculi

U2 - 10.1016/j.ic.2007.11.009

DO - 10.1016/j.ic.2007.11.009

M3 - Article

VL - 207

SP - 341

EP - 368

JO - Information and Computation

T2 - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 2

ER -