Skip to content

Home

Jump to bottom
gfbee edited this page Nov 26, 2017 · 9 revisions

Types

What are the minimal examples driving extensions to the type system and changes to the algorithms?

For the simple symbolic execution: conditional and mutation look straightforward, especially because of lack of subtyping.

  • What does the algorithm produce when we mimic those in the pure core lambda calculus?

Pure Lambda Calculus

Since the only evaluation is unary application, and every value can be unary applied, evaluation can not misuse a value, so from that perspective there is only one type.

In an encoding of booleans and OO pairs, we might want to distinguish uses of the same term: (lambda (x y) x) as true, vs the message first. That appears to be where Simply Typed Lambda Calculus begins.

What are the possibilities for a type system covering only arity?

Simply Typed Lambda Calculus [λ→]

A base type Unit/Void, with a single runtime value of that type, is convenient if zero-arity functions are distinguished from constants, and also as return type for functions meant to represent only side-effects.

Sequencing, dummy variables: ToDo.

Ascription [type assertion]: ToDo.

Pierce 11.12: Lists.

  • types List[T]
  • functions and constant: empty?[T], empty[T], cons[T], first[T], rest[T]
  • typing rules appear to be equivalent to just declaring types for the functions and constants
  • ToDo: what happens when typing the Church encoding?

Subtyping

S <: T

  • S is a subtype of T
  • an S can be safely used wherever a T can : Principle of Safe Substitution
  • set view: S is a subset of T
  • Subsumption : E |- t : S, and S <: T, => E |- t : T.
  • expect it to be reflexive and transitive

Base types: can prescribe a subtype relationship.

  • Typically add a Top.

Functions: contravariant in domain, covariant in codomain.

Lists: covariant.

  • ToDo: consequences for the constant and functions.

Polymorphism

We can ask about the types of #%app, if, and set! as if they were functions, since for typing we don't care that they're not eager by-value. They're each polymorphic, but if used only with non-polymorphic types the type-checking can still work on types as values with a bottom-up evaluation.

  • app : (a b ... -> z) a b ... -> z
  • if : Boolean a a -> a
  • set! : a a -> Void
Clone this wiki locally