Abstract Data Types Existential Types
1
Existential Types and Abstraction
Christine Rizkallah
CSE, UNSW Term 3 2020
Abstract Data Types
Existential Types
Motivation
Throughout your studies, lecturers have (hopefully) expounded on the software engineering advantages of abstract data types.
So what is an abstract data type?
Definition
An abstract data type is a type defined not by its internal representation but by the operations that can be performed on it.
Typically these operations are specified using a more abstract model than the actual implementation.
2
Abstract Data Types
Existential Types
How do we do it in C?
Language Examples: C
stack.h
typedef stack_impl *Stack;
Stack empty();
Stack push(Stack, int); Stack pop(Stack, int*); bool isEmpty(Stack); void destroy(Stack);
stack.c
#include “stack.h”
struct stack_impl { int head;
Stack tail; }
Stack empty() { … } …
3
By only importing stack.h, we hide the implementation.
Abstract Data Types
Existential Types
4
Language Examples: Haskell
Define a module but restrict what is exported:
module Stack
( Stack — Cons and Nil are *not* exported , empty
, push
, pop
, isEmpty
) where
data Stack = Cons Int Stack | Nil
empty :: Stack
empty = Nil
…
Abstract Data Types
Existential Types
5
Language Examples: Java
Typically Java accomplishes this with subtype polymorphism, something we discuss in the next lecture.
public interface Stack {
public void push(int x);
public int pop() throws EmptyStackException;
public boolean isEmpty();
}
public class ListStack implements Stack {
public ListStack() { … };
…
}
Abstract Data Types
Existential Types
No luck here.
Quote
Language Examples: Python
6
“Python is very simple and nice when you start to use it, but you don’t get too far down the road, if you’re me, before you discover it has no data abstraction at all. That’s not good because big programs require modularity and encapsulation and you’d like a language that could support that.”
Barbara Liskov, The Power of Abstraction, 2013.
You don’t need static types to enforce abstraction, but it helps.
Abstract Data Types
Existential Types
7
MinHS
How can we support abstract data types in MinHS? Can we use existing features to do so? We can use parametric polymorphism:
(type S.
recfun foo push pop isEmpty empty =
let s = push empty 42 in isEmpty (fst (pop s)))
::
∀S. (S → Int → S) → (S → S × Int) → (S → Bool)
→ S
→ Bool
(push) (pop) (isEmpty) (empty)
The program foo is defined for any stack type S. Implementations of the operations must be provided as parameters.
Abstract Data Types
Existential Types
8
Modules
We would like a single value to pass around, that contains all the implementations of the stack interface. It’s too cumbersome to pass around each function implementation individually like before. This value is called a module.
Our toy foo program from earlier needs to be rewritten as: StackModule → Bool
For some type StackModule. Taking in a value of type StackModule is analogous to importing the module.
Abstract Data Types
Existential Types
9
Via Curry-Howard
Let’s translate the type of foo into a proposition, then do logical transformations to it: Perhaps do this on the whiteboard.
∀S. ((S → Int → S) → (S → S × Int) → (S → Bool) → S → Bool) (translating to logic)
∀S. ((S ⇒ Int ⇒ S) ⇒ (S ⇒ S ∧ Int) ⇒ (S ⇒ Bool) ⇒ S ⇒ Bool) (as P ⇒ Q ⇒ R = P ∧ Q ⇒ R)
∀S. ((S ⇒ Int ⇒ S) ∧ (S ⇒ S ∧ Int) ∧ (S ⇒ Bool) ∧ S ⇒ Bool) (as ∀X.(P(X) ⇒ Q) = (∃X.P(X)) ⇒ Q)
(∃S. (S ⇒ Int ⇒ S) ∧ (S ⇒ S ∧ Int) ∧ (S ⇒ Bool) ∧ S) ⇒ Bool (back to types)
(∃S. (S → Int → S) × (S → S × Int) × (S → Bool) × S) → Bool
Abstract Data Types
Existential Types
Existential Types
We have our StackModule type:
(∃S. (S → Int → S) × (S → S × Int) × (S → Bool) × S) → Bool
StackModule
But what is this ∃a. τ thing? Existential vs Universal Types
10
∀a. τ ∃a. τ
When producing a value, a is an arbitrary, unknown type. When consuming a value, a may be instantiated to any desired type.
When consuming a value, a is an arbitrary, unknown type. When producing a value, a may be instantiated to any desired type.
Abstract Data Types
Existential Types
Another, Smaller Example
An ADT Bag is specified by three operations:
1 emptyBag, which gives a new, empty bag.
2 addToBag, which adds an integer to the bag.
3 average, which gives the arithmetic mean of all integers in the bag.
What’s the type for this?
addToBag
average
BagModule = ∃B.B×(B→Int→B)×(B→Int) emptyBag
The type of a module is called its signature.
11
Abstract Data Types
Existential Types
Making a Module
We can make a value of an existential type using the Pack expression. ∆⊢τ ok ∆;Γ⊢e:ρ[a:=τ]
∆;Γ⊢(Packτ e):∃a.ρ
Just as the type ∀a. τ could be viewed as a function from a type to a value, the type
∃a. τ could be viewed as a pair of a type and a value. Example (Bag as two integers)
Pack (Int × Int) ( (0,0)
, recfunaddToBagbi=(fstb+i,sndb+1)
, recfun average b = (fst b ÷ snd b)
) :: BagModule
12
Abstract Data Types
Existential Types
Importing a Module
If we are given a module as a parameter, we can access its contents using the Open expression:
∆;Γ ⊢ e1 : ∃a. τ (∆,a bound);(Γ,x : τ) ⊢ e2 : ρ (a bound) ∈/ ∆ ∆ ⊢ ρ ok
∆;Γ⊢(Opene1 (a.x.e2)):ρ
The last two premises ensure that the type ρ does not contain the abstract type that is
only in scope inside e2.
Example (Averaging some numbers with a bag)
recfun example :: (BagModule → Int) bagM = Open bagM
(B. (empty,addToBag,average).
average (addToBag (addToBag empty 60) 30)
)
13
Abstract Data Types
Existential Types
14
In Practice
Generally, most programming languages have fairly poor support for modules.
Dynamically typed languages typically don’t support them at all1.
Haskell without extensions, Rust, C, and Go have very weak support for them.
Java and similar accomplish modularity via OOP, which don’t support existential typing in its full generality.
Languages in the ML family, like SML and OCaml have very good support for modules.
1What they call “modules” aren’t. Just like types.