The basic idea is to have a few basic building blocks:

**functions**: objects are data, blah blah, functional programming**data structs**: just structs, no behaviors or anything**assumptions**(better name needed): just about everything else

Here's the simplest data struct possible, a stateless struct to represent nothingness. It's analogous to Java's

`null`

, Python's `None`

, Haskell's `Nothing`

, etc.data Nothing

Not much there. Here's a nickname, which is just an alias for a conjunction or disjunction of assumptions.

nickname Possible[A] = A | Nothing

Note that an alias does

*not*bring any additional type safety, it's just a macro-like shortcut. A method that takes an argument

`a::Possible[Foo]`

is identical to one that takes an `a::(Foo | Nothing)`

.Okay, let's introduce an interface-like assumption:

Sizeable -> size :: Int >= 0 Sizeable -> it isEmpty = (size = 0) it notEmpty = (size > 0)

The first line defines an assumption called

`Sizeable`

, and says that anything `Sizeable`

has a method called size that returns a non-negative integer. Read it as "being Sizeable implies that there is a size greater than or equal to 0."The next block says that anything which is

`Sizeable`

can be the argument to two functions, `isEmpty`

or `notEmpty`

. Again, we'd read this as "if something is `Sizeable`

, then (1) you can ask if it's empty and (2) you can ask if it's not empty. Note that we could have put all three implications about `Sizeable`

in one block, or we could have further split them into three blocks. Assumptions are open-world; anyone can add an implication to any assumption they want.Syntax note: Whenever we declare a method in the context of an assumption, it's assumed that the first argument to that method is the object for which the assumption holds. If we want to change that behavior, we use the keyword

`it`

for that object. This works both for declaring and invoking the method.Let's define a more interesting assumption.

Stack[A] -> push A :: Stack[A] pop :: Stack[A] head :: Possible[A] Sizeable st push A -> size' = size + 1 pop -> size' = size - 1

This defines a generic assumption for a stack. If something is a

`Stack[A]`

, it implies you can push an `A`

to it (to get another `Stack[A]`

— we're working with immutable types here), or pop the top element, or get the first element if it exists. Note that head uses the `Possible[A]`

nickname. As mentioned above, this could have also been written `head :: A | Nothing`

.This assumption

*also*states that being a

`Stack[A]`

implies being `Sizeable`

. Furthermore, it establishes assumptions about what certain functions imply. When you push onto a stack, the resulting stack has a size that's 1 greater than the original stack; when you pop, the resulting size is 1 less. The keyword `st`

here is short for "such that."The

`size'`

notation here isn't just convention, it's formally significant. Remember how earlier, I said that the notation assumes an `it`

argument when talking within the context of an assumption? When working within the context of an *implication*, any word that ends in an apostrophe works in the context of that implication. So for instance, the last line could be read as "being a

`Stack[A]`

implies being a `Sizeable`

such that invoking `pop`

implies that the resulting object (which we already know is itself a `Stack[A]`

) has a `size'`

equal to the original object's `size - 1`

."This doesn't provide an implementation for the

`size`

method, mind you. What it does do is to provide an invariant that every implementation must hold, and which any user may (formally) depend on. This is by far the sketchiest part of the language in my head, and the most ambitious, so it's still pretty sketchy. But I'll write about some of my ideas in subsequent posts.In fact, it's not just that the above doesn't provide an implementation for

`size`

; it doesn't provide an implementation for `Stack[A]`

at all! We've asserted that being a `Stack[A]`

implies certain things, but we haven't shown how to actually create a `Stack[A]`

. You can think of this as being an interface or pure virtual class. I'll talk about concrete types in the next post.
## No comments:

## Post a Comment