More on Existentials

In a previous post I suggested a new (?) interpretation for pattern variables in case branches. This post is my way to understand matters more.

Let's start with the basic example

data Temp :: * where

  Kelvin :: Float -> Temp

Then Kelvin 273.2 is about the temperature at which water freezes (or dually, thaws). Okay, let's demonstrate my point by this code:

diff :: Temp -> Temp -> Bool

diff (Kelvin a) (Kelvin b) = a == b

test t = case t of { Kelvin a -> diff t (Kelvin a) }

What do you expect the function test is? Yes, the const True one! The explanation is simple, as we are in a referentially transparent context, destructuring a value by pattern matching and reconstructing it the same way from its parts creates a value undistinguishable from the original. This of course means that diff will not be able to detect a difference.

Let's switch to a different interpretation. Some oracle invokes the case branch and says: I am not allowed to tell you what it is but here is a Float named a and you can assume that Kelvin a is indistinguishable from t!

Look ma, no 'pattern matching' or 'destructuring' needed!

a may contain 3.14 or 3.15 or 100.1 or ..., ad infinitum, we simply do not know. But we know that it names a Float! It exists as a Float. Mathematically the case branch can be written as

∃a:Float (t ≡ Kelvin a) . diff t (Kelvin a)

which is the english phrase "compute diff t (Kelvin a) under the assumption that there is a Float-valued number that when passed to the function Kelvin becomes undistinguishable from the case scrutinee".

After seeing the same thing in three languages we have to reformulate it one more time. Into logic, that is the language of type theory. Types are propositions and any value one type inhabit proves the corresponding proposition. The existential quantifier (∃) above gets mapped to a dependent sum that is the input to the computation

t : Temp ⊦ 〈a : Float, proof : SomeProp(t, a)〉. diff t (Kelvin a)

I took this formulation (and other wisdom) from Appendix A of Steve Awodey's recent paper. This part unfortunately is not my strongest side. My best guess is that SomeProp(t, a) is a type that encodes the sameness fact, and depends on a. Moreover, proof is an inhabitant of that type. The 〈a : Float, proof : SomeProp(t, a)〉 construct binds two existential variables. The I hope to come up with a nicer formulation sometime. (Please comment if I got something wrong, thanks!)

After understanding this, we can advance to more involved issues, namely one level higher. Take a look at this gorgeous definition:

data Ex :: * where

  Hide :: a -> Ex

This is a pretty useless data type but should be sufficient for my purposes. Then we need a function that pattern matches on it:

f :: Ex -> Bool

f e = case e of { Hide it -> True }

We see that pattern matching unhides the hidden value. It is said that it receives an existential type in the case branch where it is bound. But you will see no type annotation on it, ever.

So, what happens in the case branch this time? While the type of it might have been known at the moment of construction, at this point the type system does not know it. So it is assumed to have some type t. After giving our unknown a name (thus qualifying it existentially) we can ponder about the value of it. This is something we have explored above already, so we can reformulate the case branch mathematically like follows:

∃a:* (true) . ∃it:a (e ≡ Hide it) . True

The first qualifier has just a trivial condition attached to it, I believe I could also have omitted it. I am on pretty thin ice at this point so I'll refrain from giving a type-theoretic transcription, but you can imagine that there will be two dependent sum binders where the first enters in the second in the classifier position.

One more closing thought on the oracles involved. They sound mysterious but they aren't at all. For example in Ωmega the oracle for values it the reduction machinery for runtime values. It is obvious how this machinery is able to look into closures and deconstruct instances of polynomial datatypes. On the type (also kind and up) level, however Ωmega resorts to narrowing, an evaluation mechanism usually employed in logic programming. In the typing rules these mechanisms do not have a place, thus how the variables get bound remains elusive to those.

Applicative Structures and Thrists

I've been toying with the idea of furnishing the the applicative framework into thrist-like clothing, with early attempts here.

Last night I might have gotten it, finally...

Here is the idea. Since function application is left-associative, but thrists are right associative, I'll reverse the application's direction to right-to-left, i.e. f a b c will become c b a f. This uglyness is another reason to finally whip up a RevThrist, which would be SNOC-like and left-associative.

We need following ingredients:

• Fun - functions perform the reduction to a new object,
• Arg - arguments successively saturate the applicable structure to the right,
• Par - partial application (or parent) initiates the reduction.

I'll explain these elements next, but first rewrite the above expression a bit to get a parentesized form (c(b(a f))), and now with roles marked up in thrist syntax:

Cons (Arg c) $ Cons (Arg b) $ Cons (Arg a) $ Cons (Fun f) Nil

Looks almost reasonable. Time to define the ingredients mentioned above. Remember, that it must be a two-parameter data type and that the types must match up between Arg c and Arg b, etc., and finally between Arg a and Fun f. This is a pretty hefty requirement!

We can attempt passing the effective application type between the ingredients, defining the data structure as

data Appli :: * → * → * where

  Fun :: (a → b) → Appli (a → b) c

  Arg :: a → Appli b (a → b)

This means functions pass their own type to the left (and ignoring what comes from the right), while arguments expect a saturable effective type from the right, store an appropriate value and propagate the remaining type to the left. This should work now: Cons (Arg 'a') $ Cons (Fun ord) Nil, with the type being Thrist Appli Int c. As you can see, no function type gets passed to the left, so you cannot prepend any more arguments.

But this all appears useless since we cannot nest things. The Par ingredient will take care of this:

Par :: Thrist Appli a c → Appli b (a → b)

Par has a double role, it acts just like an argument, but holding a thrist inside, and thus groups a sub-application.

The c type variable occurring in Par and Fun troubled me a lot, because it allows building up illegal thrists. Consider Cons (Fun f) $ Cons (Fun f) Nil. This gibberish cannot be assigned any reasonable semantics! Finally it occurred to me to use a phantom type for filling in this breach:

data Peg

Since Peg is uninhabited, no function signature can include it (unless it is a divergent one). It also ensures that the leftmost ingredient in a thrist is a function, how practial for Par! Anyway, our Appli is done now:

data Appli :: * → * → * where

  Fun :: (a → b) → Appli (a → b) Peg

  Arg :: a → Appli b (a → b)

  Par :: Thrist Appli a Peg → Appli b (a → b)

So what brave soul will try this out? Because I must confess, up to this point I've been too lazy to fire up GHC!

You might be inclined to say, why this whole circus? An awkward notation for something as simple as function application? Any Haskell implementation can do this with a beautiful syntax!

Yes, we can build up applications but can't even compute them. This is a toy at the moment. But try to pull apart an application in Haskell! You can't! Here you can add an evaluator (foldlThrist?) and also instrument, trace, debug your evaluation process.

Also, there is a reason I say 'Applicative Structures' in the title. Here is a generalization of Appli that is parametrized:

data Appli :: (* → * → *) → * → * → * where

  Fun :: (a ~> b) → Appli (~>) (a ~> b) Peg

  Arg :: a → Appli (~>) b (a ~> b)

  Par :: Thrist (Appli (~>)) a Peg → Appli (~>) b (a ~> b)

You are free now to create your own function and value space with attached typing rules and still be able to use Thrist (Appli MySpace)...

The possibilities are endless, e.g. encrypted execution on remote hosts or abstract interpretation, you say it.

Have Fun!

Type Synonyms Generalized

Type functions are the new trend. Ωmega has them with the following syntax:

tfun :: Nat ~> Nat

{tfun Z} = S Z

Haskell (that is GHC) has them in the flavor of type families.

It has just occurred to me that they can be considered as a syntactic relaxation of type synonyms! Look:

tfun :: Nat ~> Nat

type tfun Z = S Z

type tfun (S n) = Z

When conventional type synonyms are used they must be fully applied. This should be the case here too. I am not sure whether type families or Ωmega-style type functions can be partially applied, though.

Anyway, a bit more to write at the definition site but less curlies to type at the call site; it may well be worth it.

Patterns and Existentials

I am reading papers again and this always activates my creative fantasy. I want to explain a small revelation I had just now.

Patterns are the same thing as declaring existential values corresponding to all pattern variables according to their respective types as stated in their respective constructors and asserting that the pattern interpreted as a value is the same as the scrutinee.

The body behind the pattern in turn is similarly evaluated with the existential variables in scope. Of course the existential values are filled in by some oracle which is uninteresting from the typing perspective. A strong corollary of the asserted value identity is that we can also assert that the type of the scrutinee unifies with the type of the pattern-value (in the scope of the existentials, but not outside of it)!

Just as universally quantified values are typed by dependent products (∏-stuff) the existentially quantified values are typed by dependent sums (∑-stuff). Note that the stuff is at stratum 1, e.g. types. This is in contrast to the Haskell data declaration

data Foo = forall a . Foo a

where a is at stratum 1, being an existential type.

Hmm, when thinking this to the end we may either end up at the conventional non-inference for GADTs or something like the generalized existentials as proposed in Chuan-kai Lin's thesis.

I conjecture also that this is the same thing as the post-facto type inference I suggested here.

Now all remains to is to reinterpret function calls as a data type being a tuple with existential values and to apply the above trick.

Hats off

The types subreddit references Chuan-kai Lin's PhD thesis about GADT type inference. I already have read the pointwise paper, but this is of course a revelation. He actually did implement an algorithm that inferred types for 25 (out of 30) little benchmark programs with GADTs. Previous attempts accomplished at most one!

But the thing that impressed me the most wasn't the technical side of his story but the beautifully crafted slides of his PhD defense talk. I am baffled...

Congratulations Chuan-kai!

Cooperation

I have just uploaded the thrist-0.2 package to hackage. All credit goes to Brandon Simmons, who has added significant functionality and now provides some functions for thrists that are more in line with the prelude. Brandon has accepted to be a co-author to the library and I am very happy about it. Welcome, Brandon!

For the users of the package this is good news, as I am a little dim spot on the outer sectors of the haskell radar, while Brandon is a savvy and ambitioned person, and to continue with my previous metaphor, a bright green dot on the screen, swiftly moving towards the center :-)

This post is a kind of mini release note for the release. Being an experimental package we do not intend to guarantee API stability, so we took the freedom to rename routines to make naming more consistent with the prelude. foldThrist is now foldrThrist and it got a bunch of new cousins too. Notably the types are much wider now, which allows for some more magic to happen. Finally, the haddock comments have been enhanced and as-of-present actually tell something.

Please ignore the sub-modules for now, they are unfinished, and much more experimental than the rest (I have not got around researching a compelling solution yet). A RevThrist (or similar) GADT did not make it into the release, I hope I can cram it in sometime later.

Anyway, enjoy the lib!