Dynamic arrays with curried operations

Domain Array = Nat ? A

(where A is a domain with an error element)

Operations

newarray: Array
newarray = ? n.error

access: Nat ? Array ? A

access = ? n. ? r.r(n)

update: Nat ? A ? Array ? Array

update = ? n. ? v. ? r.[n ? v]r

Previous slide

Next slide

Back to first slide

View graphic version