[Haskell-cafe] Type-directed functions with data kinds

[Adam Gundry]

Hi Paul,

On 25/10/12 16:22, Paul Visschers wrote:
> Hello everyone,
> 
> I've been playing around with the data kinds extension to implement
> vectors that have a known length at compile time. Some simple code to
> illustrate:
> [...]
> In this code I have defined a repeat function that works in a similar
> way to the one in the prelude, except that the length of the resulting
> vector is determined by the type of the result. I would have hoped that
> its type would become 'repeat :: a -> Vector n a', yet it is 'repeat ::
> VectorRepeat n => a -> Vector n a'. As far as I can tell, this class
> constraint should no longer be necessary, as all possible values for 'n'
> are an instance of this class. I actually really just want to define a
> closed type-directed function and would rather not (ab)use the type
> class system at all.
> 
> Is there a way to write the repeat function so that it has the type
> 'repeat :: a -> Vector n a' that I've missed? If not, is this just
> because it isn't implemented or are there conceptual caveats?

As Iavor, Andres and Pedro have collectively pointed out, the type

forall a (n :: Nat) . a -> Vector n a

is uninhabited, because there is no way for the function's runtime
behaviour to depend on the value of `n', and hence produce a vector of
the correct length.

Morally, this function requires a dependent product (Pi-type), rather
than an intersection (forall), so we would like to write something like
this:

repeat :: forall a . pi (n :: Nat) . a -> Vector n a
repeat Zero      _ = Nil
repeat (Succ n)  x = Cons x (repeat n x)

Notice that Pi-types bind a type variable (like forall) but also allow
pattern-matching at the term level.

Your `VectorRepeat' type class and Iavor's `SNat' singleton family are
both ways of encoding Pi-types, at the cost of duplicated definitions,
by linking a term-level witness (the dictionary or singleton data
constructor) with a type-level Nat.

As you can see, things get a lot neater with proper Pi; unfortunately it
is not yet implemented in GHC, and it's probably still a way off. I'm
working on a story about adding Pi to System FC, which hopefully might
bring it closer. (Shameless plug: for an unprincipled hack that does
some of this, check out <https://github.com/adamgundry/inch/>.)

Cheers,

Adam