Paso

Review
An exemple in a concret case
- Dynamic Fibonacci

Review

Paso is a meta and functional programming language with a strong static inferred and iso-polymorphic type system

This is how i describe Paso. But… what’s this stupid iso before polymorphic !!? Calm down please

In fact this is pretty simple, look at this code :

data Cats = Meow
data Dogs = Woof

needToEat :: Dogs -> IO ()
needToEat _ = putStrLn "Is eating"

For people who are not mad scientists and cannot read haskell, this code :

Creates 2 types Cats and Dogs, with as constructor (a way to build a value of this type) respectively Meow and Woof.
Then there is a needToEat function, it takes a Dogs and makes it eat.

But there is an important problem ! How a cat can eat with this program ? This is terrible :(

This is where paso provides a solution! (haskell too, but shhh, it’s my readme I do what I want)

What’s an isomorphism between types ?

Let’s take the Cats and Dogs types. Spoiler: They are isomorphic. But why?

Two types A and B are isomorphic means: exists (f : A → B, g : B → A) such as (f . g) ≡ idA and (g . f) ≡ idB

In other words, there must be two functions f and g. f map from A to B and g from B to A (the names of the functions do not matter) And two rules must be respected:

f . g must be equivalent to the identity of A
g . f must be equivalent to the identity of B

Yes, it looks like a bijection.

So now, let’s implement f : Cats -> Dogs and g : Dogs -> Cats

f :: Cats -> Dogs
f _ = Woof

g :: Dogs -> Cats
g _ = Meow

-- Let verify the identity law
-- (f . g) Woof = (\_ -> (\_ -> Woof) Meow) Woof
--              = (\_ -> Woof) Meow
--              = Woof
-- (Same for (g . f))
-- Works !

How Paso uses it ?

Let’s go back to the problem of cats who can’t eat, and solve it with Paso :

type Cats := { Meow }
type Dogs := { Woof }

define auto Cats ~ Dogs

needToEat : { A ~ Dogs } => A -> Effect -- or just needToEat : ~Dogs -> Effect
needToEat _ := { print "Is eating"; }

We proof just below that Cats and Dogs are isomorphic.

A ~ Dogs means forall type A isomorphic to Dogs So, we can pass Meow to this function, this is amazing ! Cat can finally eat

And now you’ve got cats thanks to paso, isn’t that amazing!

What’s subtyping ? Do you mean coercing ?

Now, paso allow us to handle isomorphism in our progam at first level. But there is a problem : Isomorphisms are quite rare. Let’s assume two new types :

data Fishes = Salmon | Shark  | Carp
data Birds  = Phoenix| Aviary | Starling | Owl
-- There are two secrets in the definition of Birds

They are not isomorphic (If you disagree, try implementing f and g in both cases). But, there is something we can do safely : We can obtain a bird from a fish.

That’s true, look at these functions :

f :: Fishes -> Birds
f Salmon = Phoenix
f Shark  = Aviary
f Carp   = Starling

g :: Birds -> Fishes
g Phoenix  = Salmon
g Aviary   = Shark 
g Starling = Carp

Notice two things :

g is partial but not f
(f . g) is an identity for Fishes type

In fact, this is just like an isomorphism but we do not need to respect the two identity law (from Birds and Fishes), but just one of them.

In Paso we call it Coerce, we write it A ~> B, and we read it I can safely get a B from a A or A can coerce to B.

If you have some intuition you had probably remark :

It looks like an injection
This is very similar to subtyping

In a more formal way : A ~> B ⇔ exists f : A → B and g : B → A such as (f . g) ≡ idA

An exemple in a concret case

Dynamic Fibonacci

fiboN : { A ~> Int } => A -> Int -- compute the n-th element of fibonacci sequence in a dynamic way
fiboN n := {
    let go n list := {
        if match list
        | (x :> y :> z) => {
            if (n == 0) | { x; }
                        | { go (n - 1) [y ; x + y ; z]; }
            }
        | _             => { noway; }
    }
    if (n >= 0) | { go n [0 ; 1 ; 0]; } | { -1; }
}

SimonHauguel/Paso