[Haskell-cafe] Type-directed functions

[Julian Arni]

Hi all,

I've been playing around with what might be described as type-directed
functions. One example is a list-like structure of phantom-typed values

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}

import GHC.TypeLits

infixr 6 :::
data a ::: b = a ::: b
             deriving (Show, Eq)

data Tag b = Tag String
           deriving (Show, Eq)

ex1 :: Tag 5 ::: Tag 3 ::: Tag 7
ex1 = Tag "Alice" ::: Tag "Bob" ::: Tag "Carol"


And then sorting 'ex1' based on the Nats, such that

sort ex1 :: Tag 3 ::: Tag 5 ::: Tag 7
sort ex1 = Tag "Bob" ::: Tag "Alice" ::: Tag "Carol"

Notice how it's the types, not the values, that determine the result, but
that the value-level also changes.

I know how to do this using classes, but it's a little excruciating - it's
like programming in a verbose and very restricted Prolog. With type families
it's much easier to get the result *type* (pattern matching is simple,
recursive calls are natural, and it all looks a lot more like Haskell), but
I haven't yet seen a way of effectively using type families to direct
the value-level component of the calculation.

Are there any examples of how this might be done? Or are there other
alternatives to using type-classes that I am missing? Or, alternatively, are
there libraries to reduce the boilerplate of this type-class code?

Thanks,
  Julian
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141230/a23b8349/attachment.html>