to make a statically known sized non-empty list
Hi haskell-cafe, so for fun and profit I was trying to make a non-empty list data type, where the size of the non-empty prefix would be known for the type-system with the following code, but it fails with an error "No instance for (Functor (NonEmpty * a)) ..." for the last line. To me it seems that all should be known, but something must be missing.. data Nat = Zero | Succ Nat data family NonEmpty (n :: Nat) a data instance NonEmpty Zero a = Tail [a] data instance NonEmpty (Succ n) a = Head a (NonEmpty n a) instance Functor (NonEmpty Zero) where fmap f (Tail xs) = Tail (fmap f xs) instance Functor (NonEmpty (Succ a)) where fmap f (Head x xs) = Head (f x) (fmap f xs) -- Markus Läll
Hi Markus, You need to add a Functor constraint for the fmap you use on the right-hand side, since that Head constructor isn't providing one (I'm not sure you can do data-families + GADTs). In other words: instance Functor (NonEmpty a) => Functor (NonEmpty (Succ a)) where Regards, Adam
Hi Markus, Rather than doing this... On 24/10/13 21:35, Markus Läll wrote:
data Nat = Zero | Succ Nat
data family NonEmpty (n :: Nat) a data instance NonEmpty Zero a = Tail [a] data instance NonEmpty (Succ n) a = Head a (NonEmpty n a)
instance Functor (NonEmpty Zero) where fmap f (Tail xs) = Tail (fmap f xs) instance Functor (NonEmpty (Succ a)) where fmap f (Head x xs) = Head (f x) (fmap f xs)
...you are probably better off using a GADT like this: data NonEmpty2 (n :: Nat) a where Tail2 :: [a] -> NonEmpty2 Zero a Head2 :: a -> NonEmpty2 n a -> NonEmpty2 (Succ n) a Now you can pattern-match on something of type `NonEmpty2 n a` in order to learn more about the value of `n`, whereas with a data family, you need to know the value of `n` in advance. This makes it harder to use. For example, it is easy to convert in one direction: convert :: NonEmpty2 n a -> NonEmpty n a convert (Tail2 xs) = Tail xs convert (Head2 x xs) = Head x (convert xs) but going in the other direction is more complicated, and requires some kind of dependent pi-type or singleton construction. Hope this helps, Adam -- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/
Hi Adam, thank you for the idea, I'll try it out later today!
On Fri, Oct 25, 2013 at 10:43 AM, Adam Gundry
Hi Markus,
Rather than doing this...
On 24/10/13 21:35, Markus Läll wrote:
data Nat = Zero | Succ Nat
data family NonEmpty (n :: Nat) a data instance NonEmpty Zero a = Tail [a] data instance NonEmpty (Succ n) a = Head a (NonEmpty n a)
instance Functor (NonEmpty Zero) where fmap f (Tail xs) = Tail (fmap f xs) instance Functor (NonEmpty (Succ a)) where fmap f (Head x xs) = Head (f x) (fmap f xs)
...you are probably better off using a GADT like this:
data NonEmpty2 (n :: Nat) a where Tail2 :: [a] -> NonEmpty2 Zero a Head2 :: a -> NonEmpty2 n a -> NonEmpty2 (Succ n) a
Now you can pattern-match on something of type `NonEmpty2 n a` in order to learn more about the value of `n`, whereas with a data family, you need to know the value of `n` in advance. This makes it harder to use. For example, it is easy to convert in one direction:
convert :: NonEmpty2 n a -> NonEmpty n a convert (Tail2 xs) = Tail xs convert (Head2 x xs) = Head x (convert xs)
but going in the other direction is more complicated, and requires some kind of dependent pi-type or singleton construction.
Hope this helps,
Adam
-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/
-- Markus Läll
participants (3)
-
Adam Gundry -
adam vogt -
Markus Läll