[Haskell-cafe] to make a statically known sized non-empty list

[Markus Läll]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20131025/d49f20d6/attachment.html>