I mean that [] is a 1D list and [[b]] is a 2D list. This is what I mean.
Even in Java,
int[][] empty = {};
is valid, and different from
int[][] notSoEmpty = { {} };
. That’s the equivalent of [] :: [[b]] versus [[]] :: [[b]].
1 Like
[] isn’t a 1D list… It depends Its type. Look at the python example, it is the same in pretty much every language I know. Probably you are getting confused by punning. This symbol [] Is commonly called Nil or Nullin other languages. Keep in mind that [a] is a linked list, so the “empty list” [] is the equivalent to the null pointer. The implementation detail isn’t relevant here…
2 Likes
It’s woth being a bit careful with your language here.
In Haskell, it’s not quite right to say [] is a “1D List”; it’s better to say it is merely “the empty list”.
Really; 2D lists and so on are a bit misleading to think of here. For example; this list:
[ [1], [1,2] ]
is it 1D or 2D ?
I would argue it’s neither; or at the very least, it’s certainly not 2D 
It’s better to talk about 2D or higher “arrays”, in Haskell, say, where each index is actually addressable, and you would define the total dimension up front. For example, the HMatrix library (see a recent blog post - Hmatrix - from zeros to hero · Nicolas Audinet de Pieuchon).
I think a big part of your confusion comes from this misunderstanding that you’re saying anything about the “depth” of a “list” when you say [a]. You are merely saying “I at least know I have a list of a's; precisely what a is I cannot say”.
3 Likes
Why does
[] :: [[b]]work?
Let’s translate into the language of data List a = Nil | Cons a (List a). That would yield
Nil :: List (List b)
The type List (List b) has the constructors Nil :: List (List b) and Cons :: List b -> List (List b) -> List (List b). So [] is really the empty list of (lists of b). The type List a and List (List a) are different and the expression ([] :: [a]) == ([] :: [[a]]) produces a type error.
Every value you use in the language is a constant. The type for every specific value is also constant: you can only narrow it down, expanding it makes no sense.
Think of it in boring mathematical terms. If you have two statements,
x + y = 3
x = 1
you are free to infer that y = 2 and there is no real reason to refer to those constants as x and y anymore.
NOTE: there are ways to break out of this, existential quantification and unsafe coercions are a part of the language, but you don’t need to bother with that in the first several years of learning the language.
Constants, once again: f :: [a] can be used both as f :: [Int] or f :: [[b]], but the narrowed down definition cannot be expanded back to [a].
No(yes, but not the way you want).
You are looking for the Smart constructors wiki entry.
The language does not provide any means to do size-checking directly at the type level, so the compile-time solution is clumsy and slow, noone uses that. The need to do runtime checks manually may seem underwhelming, but you’d be surprised how few of them you actually need in the real world.
This may or may not be helpful, but at least for me, I find it clarifying to read [a] as:
"for all a, where a is a type, the type which contains values that are lists of a".
(Indeed, in Haskell, you can write [a] more explicitly as forall (a :: Type). [a].).
Reading this definition carefully, you’ll see that it rules out lists like [True, 1, "cat"] (i.e. heterogenous lists).
Also reading it carefully, you’ll see that [1] :: [a] cannot make sense. [1] is a list with a particular type, but [a] is a type that can only be assigned to lists whose values can take all types. There’s only one such list, namely the trivial list []. Because it contains no values, all of its values can take any type.
So on reflection, while the behavior of types might look surprising at first, there isn’t really anything ad-hoc in the definition.
It might help also to separate the issue into two different things. One is universal quantification in types For example, one can write id :: a -> a, but not 5 :: a. First convince yourself that this is ok. The second there are types which take types as arguments, like if Int is a type, [Int] and Int -> Int are also types. [a] combines these two features of the type system, so it’s important to feel ok with each separately first.
I sense that part of what’s bothering you is roughly: “what’s even the point of having a type [a] if I can’t use it for e.g. 5 :: [a].”. That makes sense, but in Haskell, this isn’t the use of universal quantification (polymorphism). Instead, the use case is for things like functions, e.g. head :: [a] -> a. This function takes a list of any type a, and returns an a (or throws an exception when the input is empty). So head [True] :: Int and head ["cat"] :: String.
Yes, got that right . It is now clear how [a] works. Thank you