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.

Generalized Monads --> Gonads :-)

Here is the usual (basic) definition of monads:

class Monad m where
  return :: a -> m a
  (>>=) :: m a -> (a -> m b) -> m b

This is very much restricted to ordinary function types!
Let's see how this restriction can be lifted...

class Category (~>) => Geonad (g (~>)) where
  return :: a ~> g (~>) a
  (>>=) :: g (~>) a ~> (a ~> g (~>) b) ~> g (~>) b

Since the semantics of gonads are already eminently taken, I settled for the name Geonad.

No idea whether this can produce something relevant for our lives :-)

Cheers,
      Gabor

Absolutely, Positively Crazy

My previous two posts revolved around space optimizations in LLVM. The presented technique is a bit unconventional, and paired with the confusing nature of def-use chains, it can leave one quite puzzled...

Today in the LLVM IRC channel, chandlerc wondered whether I am eliminating the Value* from the Use struct. I corrected him, that, no, it is all about eliminating User*. But his question drove a nail im my head, making me think. After all, he was thinking of the def-use chain, and I was always dealing with user-use arrays. But deeply inside it is the same problem, a.k.a. the dual one:

• for a user-use array the User* for all array members is constant, while the defs (Value*-s) vary,
• for a def-use chain on the other hand the defs (Value*-s) are invariant, while the User*-s vary.

I wondered whether it is feasible to use the tagging technique to get rid of the Use::Val too? After all, it is just a linked list, and I have already demonstrated something similar in my previous posts.

It turns out that it is perfectly feasible, and the rest of this post demonstrates how...
...but please do not misunderstand, I do not propose this for LLVM (yet?).

Let's recapitulate what a def->use chain is:
There is an instruction that generates a value, thus defining it:

      +-------+
Val = | Instr |
      +-------+

Then there are other instructions which consume this value, but the above instruction only sees the Use objects chained up:

   +-------+
   | Instr |
   +----+--+
        |     +---+    +---+    +---+
        +---->|Use|--->|Use|--->|Use|---X
              +---+    +---+    +---+

The X above means that Use::Next is filled with NULL. Otherwise Use::Next obviously contains the pointer to the next Use object.
So to apply waymarking we have to get away with two obstacles:

1. There is no way to store something around the Use object (layout-wise), as we did with user-use arrays. We cannot go outside to place the Value*.
2. Def-use chains can be expanded and shrunk dynamically.

It turns out that 1) is pretty easy, we do not store NULL in the last Use's Next field, but the Value*, with the ‹fullstop› waymark. So when we see ‹fullstop›, the Value* can be extracted from the upper bits.
So, let's assume the ‹stop› and ‹0›, ‹1› waymarks are also tucked on the Use::Next fields. Like usual, given any Use* we can pick up the digits, and at the ‹stop› we convert the digits to a Value* and we are done. This is nice and dandy, until we remember 2). It appears a bit more tricky. Obviously the insertion/deletion will remove waymarks or add new ones. Our algorithm may begin producing bogus Value*-s. So is there any solution to this problem?
I believe there is. I have no proof but I conjecture that each destructive operation should simply place a ‹stop›, and when the algorithm is changed to only accept 32 digits between two ‹stop›s, then we are on the safe side. The corruption gets detected, an uncorrupted segment can still be found, downstream. The corruption can be repaired later (e.g. when traversing the def-use chain).

Well this is not a very efficient way of doing things, so it probably only pays off when space is extremely limited and compilation/optimization speed is not paramount. But in these applications an 8-byte (down from 16/12 bytes) Use struct is definitely tempting.