It begins with head is a mistake! It should not be in the Prelude. Other partial Prelude functions you should almost never use include tail, init, last, and (!!). From this point on, using one of these functions on a homework assignment will lose style points!
And here is a proposal:
data NonEmptyList a = NEL a [a]
nelToList :: NonEmptyList a -> [a]
nelToList (NEL x xs) = x:xs
listToNel :: [a] -> Maybe (NonEmptyList a)
listToNel [] = Nothing
listToNel (x:xs) = Just $ NEL x xs
headNEL :: NonEmptyList a -> a
headNEL (NEL a _) = a
tailNEL :: NonEmptyList a -> [a]
tailNEL (NEL _ as) = as
Dear sirs, a List is a recursive data structure by definition. Non-recursive List is an unimaginable nonsense. What was made here with a name of safe(!) NonEmptyList is some ugly Pair with lots of syntactic noise.
How could you get the last element from your NonEmptyList? How could you tell how many elements in it?)
But, of course, never ever use these ugly unsafe lists - they might be empty! Use safe NonEmptyList because in Haskell everything is safe. And never try to think what the fuck you are reading.
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.
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
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.
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.
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.
I don't see that answer arguing that `safeHead` is bad. Russell O'Connor just seems to be arguing that it'd not be possible for `head :: [a] -> a` to have a sentinel value `uhOh :: forall a . a` which you could pattern match on when `head []` is called... but `safeHead :: [a] -> Maybe a` is just fine since it has a different free theorem.
In the comments on Real World Haskell people (Alex Stangl and Paul Johnson in particular) are talking about added complexity of deferring invariant errors, but since these are type-declared via `Maybe` it really helps to add safety. I personally have written many, many functions with partial types because I had forgotten about some assumed invariants and had them fixed by use of `safeHead`.
NonEmptyList is pretty good for pre-handling all of the failure modes.
NonEmptyList is usually implemented that way to be a bit lazier on the implementation end. You can also write it as
data NEL a = One a | More a (NEL a)
but then you have to write fresh functions for all of the default list methods without any performance improvements (which make doing so totally valuable for things like Vector). You also have NEL being an instance of a more general NonEmptyFunctor pattern like in (http://hackage.haskell.org/packages/archive/non-empty/0.1.3/...).
With this recursive NEL, last is
last :: NEL a -> a
last (One a) = a
last (More _ more) = last more
and (inefficient, corecursive) length is
len :: NEL a -> Int
len (One _) = 1
len (More _ more) = succ (len more)
NELs are quite useful not just for safety. head as type [a] -> a is largely considered to be a mistake, the Safe package is quite popular and redefines head as having type [a] -> Maybe a. I use it frequently.
NELs have properties like being Semigroups (and not Monoids) and Comonads which regular lists do not. This helps not only for theoretical guarantees of safety but also so that we can feel confident that our typeclass declarations have the meaning they're supposed to have.
So is (NEL a = NEL a [a]) a bad solution? It's perhaps less independently beautiful than the truly recursive NEL, but it's easier to write and takes advantage of Haskell's built in "possibly empty List" functionality. It's also more "globally beautiful" in that it fits into the family of types "non-empty functors". The recursive version is also trivially isomorphic, so there's no loss in functionality.
NEL was provided as an example to think about, not as a 'proposal'. There was no suggestion that students use this for everything.
Keep in mind that this is a structured 100-level class targeted at undergrads who are relatively new to programming and haven't seen much in the way of functional programming and Hindley-Milner typing.
It begins with head is a mistake! It should not be in the Prelude. Other partial Prelude functions you should almost never use include tail, init, last, and (!!). From this point on, using one of these functions on a homework assignment will lose style points!
And here is a proposal:
Dear sirs, a List is a recursive data structure by definition. Non-recursive List is an unimaginable nonsense. What was made here with a name of safe(!) NonEmptyList is some ugly Pair with lots of syntactic noise.How could you get the last element from your NonEmptyList? How could you tell how many elements in it?)
But, of course, never ever use these ugly unsafe lists - they might be empty! Use safe NonEmptyList because in Haskell everything is safe. And never try to think what the fuck you are reading.