Paul Visschers | 25 Oct 17:22 2012
Picon

Type-directed functions with data kinds

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:
> {-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
> import Prelude hiding (repeat)
> data Nat = Zero | Succ Nat
> data Vector (n :: Nat) a where
>   Nil :: Vector Zero a
>   Cons :: a -> Vector n a -> Vector (Succ n) a
> class VectorRepeat (n :: Nat) where
>   repeat :: a -> Vector n a
> instance VectorRepeat Zero where
>   repeat _ = Nil
> instance VectorRepeat n => VectorRepeat (Succ n) where
>   repeat x = Cons x (repeat x)

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?

Paul Visschers
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Iavor Diatchki | 25 Oct 17:56 2012
Picon

Re: Type-directed functions with data kinds

Hello Paul,


If you don't want to use the class system, you could write `repeat` with a type like this:

    repeat :: Proxy n -> a -> Vector n a

(`Proxy` is the singleton family 'data Proxy n = Proxy`).

You can't really do it with a function of type `a -> Vector n a` because there is no way for the function to know how many elements to generate. 
You cannot determine the length from the type `n` because polymorphism in Haskell is _parametric_, which means that the function needs to behave uniformly for all types.
This is nice because it makes reasoning about programs easier, but also, it allows for efficient implementation---there is no need to pass type-representations at run-time.
In contrast, overloaded values may behave differently depending on their type, just like your implementation of `repeat` below.  This is perfectly OK, and it is clearly marked in the type.


I hope this helps,
-Iavor



On Thu, Oct 25, 2012 at 8:22 AM, Paul Visschers <mail <at> paulvisschers.net> 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:
> {-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
> import Prelude hiding (repeat)
> data Nat = Zero | Succ Nat
> data Vector (n :: Nat) a where
>   Nil :: Vector Zero a
>   Cons :: a -> Vector n a -> Vector (Succ n) a
> class VectorRepeat (n :: Nat) where
>   repeat :: a -> Vector n a
> instance VectorRepeat Zero where
>   repeat _ = Nil
> instance VectorRepeat n => VectorRepeat (Succ n) where
>   repeat x = Cons x (repeat x)

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?

Paul Visschers

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Andres Löh | 25 Oct 18:03 2012
Picon

Re: Type-directed functions with data kinds

Hi Iavor.

> If you don't want to use the class system, you could write `repeat` with a
> type like this:
>
>     repeat :: Proxy n -> a -> Vector n a
>
> (`Proxy` is the singleton family 'data Proxy n = Proxy`).

How is the polymorphism becoming any less parametric by using this
particular Proxy type?

Cheers,
  Andres
Iavor Diatchki | 25 Oct 18:21 2012
Picon

Re: Type-directed functions with data kinds

Hello,


Sorry, I made a mistake, the version of 'repeat :: Proxy n -> a -> Vector n a' won't work either, as Andres noticed, because `Proxy` still won't give you information about how many times to repeat.
You'd have to use a structured singleton family, where the values are linked to the types:

data SNat :: Nat -> * where
  SZero :: SNat Zero
  SSucc :: SNat n -> SNat (Succ n)

repeat :: SNat n -> a -> Vector n a 

Apologies for the confusion,
-Iavor





On Thu, Oct 25, 2012 at 9:03 AM, Andres Löh <andres.loeh <at> gmail.com> wrote:
Hi Iavor.

> If you don't want to use the class system, you could write `repeat` with a
> type like this:
>
>     repeat :: Proxy n -> a -> Vector n a
>
> (`Proxy` is the singleton family 'data Proxy n = Proxy`).

How is the polymorphism becoming any less parametric by using this
particular Proxy type?

Cheers,
  Andres

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
José Pedro Magalhães | 25 Oct 19:43 2012
Picon

Re: Type-directed functions with data kinds

Hi Paul,

On Thu, Oct 25, 2012 at 4:22 PM, Paul Visschers <mail <at> paulvisschers.net> 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:
> {-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
> import Prelude hiding (repeat)
> data Nat = Zero | Succ Nat
> data Vector (n :: Nat) a where
>   Nil :: Vector Zero a
>   Cons :: a -> Vector n a -> Vector (Succ n) a
> class VectorRepeat (n :: Nat) where
>   repeat :: a -> Vector n a
> instance VectorRepeat Zero where
>   repeat _ = Nil
> instance VectorRepeat n => VectorRepeat (Succ n) where
>   repeat x = Cons x (repeat x)

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?

There are conceptual caveats; see http://hackage.haskell.org/trac/ghc/ticket/6074 (particularly the comments).
This would require fundamentally changing the way in which constraints are elaborated into core code.


Cheers,
Pedro
 

Paul Visschers

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Adam Gundry | 26 Oct 09:25 2012
Picon
Picon

Re: Type-directed functions with data kinds

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
Paul Visschers | 27 Oct 10:22 2012
Picon

Re: Type-directed functions with data kinds

Thanks for all the replies. I guess I'll keep using my type class for now.


Paul

On Fri, Oct 26, 2012 at 9:25 AM, Adam Gundry <adam.gundry <at> strath.ac.uk> wrote:
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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane