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!