Pattern musings

A new breed of patterns

I like to code up little snippets in Haskell to play around with interesting concepts. Sometimes I invent notation that must appear forcing to most, but let's introduce it anyway...

How I use ViewPatterns, for fun and profit

When writing evaluators, I like to use view patterns to evaluate subtrees already on the LHS (pattern side). Let's introduce a mini-language (also called Hutton's razor) that can only add:

data AST = Lit Integer | Plus AST AST deriving Show

The evaluator is maximally simple, as it only needs to care about two sole cases:

eval :: AST -> Integer

eval (Lit res) = res

eval (Plus l r) = eval l + eval r

There is a train of thought that cares about termination and logical consistency and thus requires that in the definition of eval (Plus l r) the function to be defined can only be applied to structurally strictly smaller arguments (these are the hypotheses). We adhere to this rule above, but for more complicated functions it is possible to introduce bugs when not being super careful.

So why not resort to view patterns, and ban the eval from the RHS altogether?

eval (Plus (eval -> l) (eval -> r)) = l + r

This way of putting it makes it totally clear that eval is always applied to parts of the syntax tree.

Result patterns?

But let's return to the base case (Lit). We are forced to come up with a new binding (res), just to have something in our hands that we can return? Sounds like redundancy. So for the purpose of this post I'll come up with a result pattern (=), which can appear on the LHS only once and it's presence there will rule out the RHS:

eval (Lit =)

No more arbitrary names!

View lambdas, anyone?

Okay, so let's turn up the heat a bit more. A continuation-passing interpreter is a tail recursive way to evaluate the AST:

cps :: forall k. AST -> (Integer -> k) -> k

cps (Lit n) k = k n

cps (Plus l r) k = cps l (\l -> cps r (\r -> k $ l + r))

For the purpose of this exercise you can consider the type k to be unit (), and the continuation (value k) a consumer of intermediate results. We recognise the same usage pattern as in eval: subtrees are immediately (and linearly) passed to the function to be defined. So let's rewrite it with view patterns:

cps (Plus (cps -> l) (cps -> r)) k = l (\l -> r (\r -> k $ l + r))

But  now we face the same redundancy issue, that the view patterns bind identifiers that are somehow repetitive, as they are applied to lambdas immediately. Can we come up with a notation for a view pattern that applies on a lambda and extends its scope to the rest of the patterns and to the RHS? Consider

cps (Plus (cps -> \l) (cps -> \r)) k = k (l + r)

It takes some time to see the charm here, as it is wormholing a lambda-bound identifier to the RHS, but it is unbeatably concise. And we can combine it with the result pattern idea too:

cps (Plus (cps -> \l) (cps -> \r)) (($ l + r) -> =)

At this point however the readability is suffering.

Outro

Note that the view lambdas are strange beasts, not only because they wrap the result (RHS or = pattern), but also the identity holds: \p ≡ (id -> \p), but since all the ids don't change anything, they can be stripped anyway. I wonder where I shall encounter more such view lambdas in the wild...

Unembedded associations

Everytime I start understanding the gist of a paper that appeared unfathomable to me a few months before, a strange thing happens to me. My brain often wanders off, and creates interesting new bridges, on which my thoughts begin to run and reach new previously unchartered land. This same thing happened to me when reading Atkey et al.'s "Unembedding Domain-Specific Languages". Here I encountered my old friend, the HOAS lambda vocabulary

class LC expr where
  lam :: (expr → expr) → expr
  app :: expr → expr → expr


Freely associating I came up with an idea how to simulate a limited form of duck typing for conditionals:

class Condition expr
  toBool :: expr → Bool
  cond :: expr → a → a → a
  cond c th el = if toBool c then th else el


This would allow to retrofit many condition-like data types with this vocabulary. Nothing, 0, (Left _) all could serve as false.

Maybe I could even follow Conor McBride's advice and make the then and else arms of the conditional differently typed. Though I would need associated types for that.

Duck typing may turn out like a good idea in a statically typed language, when implemented this way. Another use case would be function application by the built-in juxtaposition syntax. It already means different things in different syntactic contexts, like function application or type (family) application. Idiom brackets come to my mind. Edward Kmett's Apply class looks like a good candidate for a related vocabulary. The typing rule would be implemented by an associated (injective) type family. Hopefully someday we'll see -XRebindableSyntax for value-level application, that is type-directed.

gdiff – Polymorphically

In the few last months I've been busy coming up with techniques mastering the gdiff Haskell library, even for use cases it was not originally designed for.
This is mostly a brain dump of some approaches I have learnt while tinkering and trying to solve certain problems.

1) Polymorphic diff: Eelco Lempsink writes in the conclusion of his 2010 thesis «Furthermore, we can not encode polymorphic datatypes such as lists, but need to write specific encodings for each type we want to include». In the library documentation he says «It might require another master thesis project to solve this». However in the last days I developed a trick, which does allow me to describe polymorphic data types, such as [a] or Maybe a. I just needed to add these lines:

in the family GADT:
  ListNil :: List Fam as → Fam a as → Fam [a] Nil
  ListCons :: List Fam as → Fam a as → Fam [a] (a `Cons` [a] `Cons` Nil)

then define a Type instance:
instance Type Fam a ⇒ Type Fam [a] where
  constructors = head [Concr (ListNil cc) | Concr cc Concr cc ← constructors] : [head [Concr (ListCons cc) | Concr cc ← constructors]]

What is this doing? It picks two random constructors from the underlying data type and wraps them with ListNil and ListCons. We usually ignore what is wrapped, with one exception: in decEq one needs to ensure that the constructors' arguments are compared too, otherwise one cannot finish the type equality proof.

2) Non-moving pairs: In the usual textual diff algorithm the lines may move around a bit to make room for insertions, etc. This is normally the case for gdiff too. I have seen gdiff reusing values (with Cpy) when comparing (True, False) with (False, True). But sometimes this is not desired at all. I figured out that "inlining" the leaves into the pair's description (i.e. instead of (a `Cons` b `Cons` Nil) writing appendList on the field decompositions of a and b does the trick.

3) Location types: I found a way to equip Abstr constructor descriptors with type class dictionaries. It is similar to the lifting approach shown under 1), but much more involved.
The idea is to wrap a location-aware descriptor with a descriptor that is location-blind, i.e. that hides the location parameter: Loc' :: KnownNat n ⇒ Fam (Loc n Bool) …
Then we need the wrapper:
Hidden' :: KnownNat n ⇒ Fam (Loc n Bool) ts → Fam (Hidden Loc) ts
Giving the Type instance for the latter is tricky, as Abstr alone has no provision for dodging the class dictionary into Hidden', so I had to write a locAware smart constructor to syphon it through the Hidden' wrapper.
This also stressed the compiler to its limits in the advanced PolyKind-ed approach I needed, so I filed a GHC bug #9725. There is also some code showing how the Hidden Loc is unwrapped and the dictionary-passing functions is installed into the Abstr.

4) Monadic actions coming out of patch: Here another wrapping approach is needed, but this time we need a sum type for diff and patch so that we can enter with a pure value at the Left and obtain a Right action back. This is the most involved approach. I can probably blog another time about it.

First Programming with my Daughter

Today I had a short programming session with my 7 year old. I had shown her earlier what a list is and she came back several times already to show her "more lists".
So this time I thought we could do something more interesting. A letter-changing game! I fired up GHCi and entered:

Prelude⟩ let satz = "Leleka hat Kacke in der Hose"
Prelude⟩ print satz
"Leleka hat Kacke in der Hose"


She loved it so far. Fun is the strongest motivator to learn for kids…

Then came the changer for letters:

Prelude⟩ let tausch = \x → case x of {'L' → 'K'; 'e' → 'i'; 'i' → 'u'; 'u' → 'e'; x → x }


Then I applied it on the phrase defined earlier:

Prelude⟩ map tausch satz
"Kilika hat Kacki un dir Hosi"


This did it. She kept repeating the transformed sentence for an hour, giggling. I tried to explain to her what we did just now, but I guess I'll wait till next time to make her repeat this exercise.

Rank-2 PHOAS

Lately I've been experimenting with finally-tagless (typed) representations and made an attempt to model the (implicitly typed) lambda calculus. However, I wanted to use the parametric higher-order abstract syntax (PHOAS) technique to obtain variable bindings that are automatically well-scoped.
I arrived at this formulation:

class LC rep where
  var :: p → rep
  lam :: (forall p . p → rep) → rep


(I am ignoring applications as they are not important for making my point.)
As Andres Löh has pointed out to me this is not the final-tagless formulation of the regular PHOAS form, as that would add the p type variable as the second class parameter and the rank-2 forall would appear from "outside".
But I liked my simple formulation and the obviously and explicitly parametric lambda body. So I started implementing a rudimentary visualisation instance given a name supply:

instance LC ([String] → String) where
  var = ??? -- const "VAR"
  lam f = \supply → ...


It turns out that implementing var is only possible by giving a constant result, and for lam I am in trouble, because I cannot call f as it expects a polymorphic argument. Both problems are due to the fact that p is too polymorphic. Can we have it a bit less polymorphic in order to make some progress?
Thinking about it I came up with the idea of giving each instance a way to constrain the p variable as it fits. So I changed class LC such:

class LC rep where
  type Restricted rep p :: Constraint
  var :: Restricted rep p ⇒ p → rep
  lam :: (forall p . Restricted rep p ⇒ p → rep) → rep


Now my instance can pick the restriction as it fits:

instance LC ([String] → String) where
  type Restricted ([String] → String) p = ([String] → String) ~ p
  var = id
  lam f = \supply → ...


As you see I chose the restriction to be type equality which essentially cancels parametricity in this instance and gives me simple HOAS. Filling in p becomes easy now.

  lam f = \(n:ns) → "\\" ++ n ++ "." ++ (f $ const n) ns

Let's try it out! But in order to do that we need an instance of Show for name supplies. This could be one:

instance Show ([String] → String) where
  show f = f $ map (('v':) . show) [0..]


Now we can interpret a lambda term as a name supply.

*Main› lam (\x → lam $ \y → var x) :: [String] → String
\v0.\v1.v0

It works™ :-)

But I can go further. After implementing several other instances I observed that I always wanted to destroy parametricity completely and implement var as the identity. So why not have these as defaults and reduce the boilerplate by a nice margin? Here is the final class definition that I arrived at:

class LC rep where
  type Restricted rep p :: Constraint
  type Restricted rep p = rep ~ p
  var :: Restricted rep p ⇒ p → rep
  default var :: rep ~ p ⇒ p → rep
  var = id
  lam :: (forall p . Restricted rep p ⇒ p → rep) → rep


I like it so far.

PS: Here are the prerequisites if you want to compile the above yourself:

{-# LANGUAGE UnicodeSyntax, ConstraintKinds, TypeFamilies, RankNTypes, FlexibleInstances, DefaultSignatures #-}

import GHC.Exts


Testing LaTeX with MathJax

$3_{5}$ $$42^{25}$$
extensions: ["tex2jax.js"], jax: ["input/TeX", "output/HTML-CSS"],
Does not work

But this:

<script src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script>

<script type='math/tex; mode=display'>   \{ 0, 1, 2 \} </script>

Results in something pretty: $$\{ 0, 1, 2 \} \mathcal{L}$$

Now it's evident — totally!

In one of my posts about logics I have shown that a proof of a true proposition consists of constructing a function from ⊤ (truth) to an inhabitant of that proposition (interpreted as a type).

Dually, one would hope, we must construct a function between false propositions and ⊥ (bottom, the empty set).

The big question is: How? There appear to be many functions into the empty set. These surely cannot mean to be proofs!

There is a catch: totality. For every possible input we are obliged to provide a well-defined, deterministic result. A hard job when the target set is empty!

On the other hand it is easy enough for positive proofs: (considering the finite case...) say, we seek a proof of the Bool proposition. Bool has two inhabitants, so the function space from ⊤ (single inhabitant) to Bool must have 2¹ of them. Here is one:

provebool () = True

(Do you find the other one?)

But for negative proofs, it isn't really obvious how to do it. Since refutable propositions (allegedly) have no inhabitants, how do we write a pattern-matching function between them?

But remember, in the finite proof case our arrows had n^m inhabitants, picking any one of these constituted a valid proof.

For the uninhabited case such a way of counting gives us a clue: 0⁰ can be interpreted as 1! And this is the key, we need to do pattern matching with no patterns to get that inhabitant:

refutation = \case of {}

When this function is total, we have our sought-for unique proof. And for actual negative proofs it evidently is!