Thursday, November 6, 2014

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.