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
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
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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
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
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
Hi Paul,
On Thu, Oct 25, 2012 at 4:22 PM, Paul Visschers
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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
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
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
participants (5)
-
Adam Gundry -
Andres Löh -
Iavor Diatchki -
José Pedro Magalhães -
Paul Visschers