On: CIS 194: Introduction to Haskell (Spring 2013)

[Peaker]

A better solution is length-encoded lists (often called Vectors):

  data Vector length a where
    Empty :: Vector 0 a
    Cons :: a -> Vector n a -> Vector (1 + n) a

But Haskell isn't very good at such encodings. Type-level computation is often not worth it.

That said, even NonEmptyList is sometimes useful. For example, some Prelude functions could use it:

  group :: [a] -> [NonEmptyList a]

Making common idioms like:

  map head . group ...

Safe again.

Not sure what you mean by:

> How could you get the last element from your NonEmptyList? How could you tell how many elements in it?) Exactly two.

  import Data.Monoid
  import Data.Maybe

  lastNel :: NonEmptyList a -> a
  lastNel (NEL x xs) = fromMaybe x . getLast $ mconcat $ map (Last . Just) xs

  lengthNel :: NonEmptyList a -> Int
  lengthNel (NEL x xs) = 1 + length xs

[jdn → Peaker]

I'm not quite sure what you've done there. You seem to be confusing type signatures with function definitions. You've also used GADT syntax, requiring -XGADTs, which isn't needed for a simple vector type.

> Cons :: a -> Vector n a --> Vector (1 + n) a

This makes no sense, you can't specify constants in a type signature, and you certainly can't add constants to a type variable in one.

I may be the one not in the know here, if so please show me this magic.

[quchen → jdn]

He used pseudo-notation for something that is possible in GHC. (1+) on type level corresponds to the successor function, and a compiling version of Peaker's code would be this:

    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    
    data Nat = Z | S Nat
    
    data Vector l a where
          Nil :: Vector Z a
          Cons :: a -> Vector l a -> Vector (S l) a

[jdn → quchen]

Thanks for this! Had looked at examples of this but it's nice to have the link to Peaker's code

[klibertp → jdn]

Not in Haskell, but there are languages where it's possible. It's called dependent typing and I don't really understand how it works, but I suppose gp was referring to this.

[sold → klibertp]

It is possible in GHC, see parent comment.

[jdn → klibertp]

Oh of course, and that also explains the use of GADTs since they are one route to dependent types in Haskell. I'm not sure what he's done there is fully legit, but maybe not as loony as at first thought.

[tel → jdn]

It plays fast and loose on notation, but is perfectly kosher in GHC (not Haskell2010 or Haskell98).

[dschiptsov → Peaker]

But these are solutions for some Array of unknown size or some abstract collection - why to call it a List? For a List the notion of the-empty-list is essential.

[Peaker → dschiptsov]

Not for the NonEmptyList...

Is your problem mainly what you call this notion?

[dschiptsov → Peaker]

I'm an old-school perfectionist, sorry.)

http://karma-engineering.com/lab/wiki/Tutorial10

[Peaker → dschiptsov]

If you have a structure whose only difference from a list is that it is guaranteed to have at least one element, why not call it a NonEmptyList?