Markus Läll | 24 Oct 22:35 2013
Picon

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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
adam vogt | 24 Oct 23:16 2013
Picon

Re: to make a statically known sized non-empty list

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
Adam Gundry | 25 Oct 09:43 2013

Re: to make a statically known sized non-empty list

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 | 25 Oct 10:13 2013
Picon

Re: to make a statically known sized non-empty list

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 <adam <at> well-typed.com> wrote:
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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane