As far as I understand [a] means that there can be a list that can have any number of nested lists inside.
f :: [a] -> a
f (x:xs) = x
It is possible to call f [[1,2]] or f [[[True]]]] without issues.
What I don’t understand on the other hand is why does [1] :: [a] give an error in the ghci.
ghci> [1] :: [a]
<interactive>:20:2: error: [GHC-39999]
* No instance for `Num a1' arising from the literal `1'
Possible fix:
add (Num a1) to the context of
an expression type signature:
forall a1. [a1]
* In the expression: 1
In the expression: [1] :: [a]
In an equation for `it': it = [1] :: [a]
How come does it work when calling a function and it does not when defining the type of a variable?
I am a beginner learning haskell so please be patient with me
There’s a few things here to help better your understanding.
First, as to your direct question, you have a list [] containing an integer literal 1. You’ve tried to assign it as a list [] that could contain anything a, where a is a type variable - so I suspect you are trying to declare a polymorphic list.
You can do this with an empty list, because an empty list can be any type of list.
ghci> [] :: [a]
[]
However, you’ve actually given it a value - an integer literal 1.
Now, this integer literal imposes a constraint on the type of values that the list can contain - it must be Num -eric, so it can’t just be a -nything. So it needs a Num a constraint a la:
ghci> [1] :: (Num a) => [a]
[1]
Aside from this, you’ve slightly confused data constructors and type constructors a little here:
[[1,2]] and [[[True]]] are the types of lists of lists (and so on), where the type of data stored in the lists is also a list.
However, a list data type is also constructed recursively, where (x:xs) is the constructor (:), and x :: a is the first thing stored in the list, and xs :: [a] is the rest of the that list. So This is different from a list that contains lists as a type (eg, [[[a]]]).
It helps to understand that (x:xs) just means Cons x xs if you define lists yourself:
data List a
= Nil
| Cons a (List a)
It contains ‘more lists’ as a recursive data type via the List a inside Cons a (List a), but it can also contain ‘more lists’ by making the contained a element type itself a list.
I hope this helps, I can explain further if you like.
Thank you very much for the comprehensive answer.
My confusion lies in why does f [1] work because the type of [1] matched the type of [a] while when writing [1] :: [a] I get an error.
As far as I know all types are erased at compile time. Maybe haskell is having a hard time knowing how to implement a list of any a
Coming from a java background [a] feels to me like saying “here is a list of Objects, put anything inside”.
In java it is perfectly fine to define a list of Objects and put an arbitrary object inside the list.
The a in [a] is a type variable. It is a place where a type has to go eventually, but we are not saying what it is yet. The actual type that goes in the place of this variable will be determined whenever it is used.
For example, when you use your function f like this: f [[1,2]] then we know that [[1,2]] has type [[Int]] and f expects and input of type [a]. We can match these types up:
[ a ]
[ [Int] ]
And so we can determine that a must be [Int].
This does rely critically on the fact that the function f works properly for any possible way you could use it. So f must work for lists with any kinds of elements in it, in this case [[Int]], but also for [Bool] or even [Int -> Bool] etc.
Your second example of [1] :: [a] does not work because the value [1] is only valid at the type [Int]. It won’t work if you give it a different type like [[Int]] or [Bool] or [Int -> Bool], so it won’t work if you give it the type [a] either.
They can be safely erased if they can be satisfied. In this case, a simple type variable a does not satisfy the constraint requirements of an integer literal 1 :: Num a => a. Give it a try by looking up it’s type with :t:
ghci> :t 1
1 :: Num a => a
NOTE: use :? to get help regarding a lot of useful GHCi commands
It needs a Num constraint that restricts the type of a to only those data types that are Num -eric, which makes sense because we know that 1 has to be a number.
Try it out with the list:
ghci> :t [1]
[1] :: Num a => [a]
Note that the f function works with any type of list because it doesn’t care anything about what a might be - it doesn’t have to be a number like [1] :: Num a => [a] did
f :: [a] -> a
f (x:xs) = x
This is why f can take any type of list, including lists of lists like [[[Int]]].
You’re confusing types and terms here. Haskell traditionally uses the same square bracket notation for both terms and types, but you could use List in the types. Then you’d get:
List a
[1]
Which doesn’t match.
My earlier example then becomes:
List a
List (List Int)
This does match and you can conclude that a is List Int.
[a] means a list where you can put anything, and you don’t know anything about the content. So you can’t for instance call map (+1) over it to add 1 to each value a, because a might not be a number. It could be, but you don’t know. It is a list, but of what?
You can still perform operations on the list, such as taking the first element using head (which is what your f function is), or by reverse -ing it, because (unlike map (+1), you don’t need to know what a list contains, to be able to do something like shuffle it. You can affect the list, but you cannot do anything with its current content.
On the other hand, Num a => [a] means a list where you can put anything that you definitely know is an instance of Num (so, a number), and so you can call map (+1) [1,2,3] to get [2,3,4] because you know they are numbers. It is a list-of-numbers, and here you can actually do something number-y to affect the contents of the list because you know that they are numbers.
Now, the thing to remember, is that you can always ‘forget’ properties for free. All lists-of-numbers are lists, so its not a problem to turn Num a => [a] into [a], but since not all lists are lists-of-numbers, you can’t turn [a] into Num a => [a] *unless you can prove they are Num -bers.
Don’t worry, learning is the process of encountering things that you do not yet understand.
@ApothecaLabs I think that I finally have some idea of how Haskell works with this types.
I am still wondering why Haskell can’t forget that the list is actually a list of numbers and treat like an arbitrary list.
It is true that not all lists are lists-of-numbers but why can’t Haskell treat a list of numbers as it would be an arbitrary list of stuff?
I come from a Java background where I can say stuff like Object x = 1; and then treat x as it would be a general object when in fact it is a number.
For me it seems that defining a general type in haskell and having a concrete variable for that type is not possible. If I try to do that, Haskell will complain that my concrete variable type is NOT the “any” type.
Basically, I think it all boils down to the question of having polymorphism for variables in Haskell.
The more appropriate Java-equivalent for this question would be something like
public <A> ArrayList<A> myList() {
final ArrayList<Integer> result = new ArrayList<>();
result.add(1);
return result;
}
This wouldn’t work in Java, because you’re returning an ArrayList<Integer>, but myList needs to return an ArrayList<A>, and nothing in the definition of myList guarantees that A is Integer (even though, somewhere else in your program, you could call myList with A corresponding to Integer).
In Haskell, type variables are like Java’s, except they aren’t limited to functions and classes only. Even individual values like [1] can have types that are parameterized by type variables. If it helps, think of terms like that as functions that take no parameters, like the myList above.
Now, on the other hand, here is some Java that does work:
public <A> void useAList(ArrayList<A> input) {
// do something with input
}
public void main() {
final ArrayList<Integer> input = new ArrayList<>();
input.add(1);
useAList(input);
}
This demonstrates that you can use an ArrayList<Integer> as an argument to a function that expects an ArrayList<A>. The same is true in Haskell: if you have a function that expects an [a], you can provide it with [1]. Haskell does let you treat a list of numbers as a list of arbitrary stuff, in this way.
So that means that I can think of polymorphic variables as functions in java that have abc and so on as generic arguments basically.
I think now it makes more sense.
From what I understand, when I see [a] that means that the type of a will be determined by the person who will call or use the function. It is like a placeholder that must be filled on the caller side and it is not filled when defining it.
Thank you @rhendric for taking the Java approach to explain this concept.
Thanks for the answer.
I understand what you are saying.
My confusion mostly relies in the fact that haskell treats [a] different when using a function paramater and when defining a local variable.
Kinda! A more accurate way to put it is that any time a term A is checked against a type T, T needs to subsume the type of A (where a type like [Int] subsumes a type like forall a. [a], but not vice-versa). But when a term with type parameters is used, those parameters are first instantiated with unknowns.
If you have f :: [a] -> a, that type (probably; there are exceptions, but I won’t go into that now) introduces a new type variable called a, just like the bare <A> at the beginning of a generic function in Java does. If you want to be explicit about this, you can write f :: forall a. [a] -> a, and that form will help me explain this better. That type variable is instantiated with an unknown everywhere f is used. The general type of f is forall a. [a] -> a, where a is a quantified type variable; but the type of a particular use of f is [a0] -> a0, where a0 is some unknown type that the compiler will have to solve.
Then when you apply f to [1], the compiler is going to try to unify what it knows of the type of [1]—namely, Num b => [b], for some unknown b—with what it knows of the type of the argument of f—namely, [a0] for some unknown a0. Noting the Num b constraint as something to be solved later, the compiler notes that [b] and [a0] are the same if and only if b and a0 are the same. Since both of these variables are unknowns, it is free to make that assumption, and then it knows that the final type of f [1] is b. (There’s some hackery that I won’t get into that enables the compiler to guess a reasonable b in this case, given the unsolved Num constraint.)
The same general thing happens if you have a term with a type annotation, like [1] :: [a]. Like before, this is implicitly [1] :: forall a. [a]. And now the compiler tries to unify the types Num b => [b] and forall a. [a]. But there’s no reference to some parameterized declaration, so instantiation doesn’t happen. And forall a. [a], in which a is not an instantiated unknown but is instead a quantified variable, doesn’t subsume Num b => [b]; the reverse is true. (In English: ‘I return a list of whatever type you want’ doesn’t subsume—isn’t a looser requirement than—‘I return a list of whatever numeric type you want’). So this gets raised as an issue.
