You've gotten confused by the (confusing) fact that []
means two different things in different contexts in Haskell, which has made it hard for you to interpret the rest of your experiments.
At the value level []
indeed is the empty constructor for lists. But when you asked for the type of Property "Colors" [1,2,3,4]
and saw Property [] a
you're looking at a type expression, not a value expression. There is no empty list at the type level.1 Instead []
is the type constructor for the list type. You can have [Int]
(the type of lists of ints), [Bool]
(the type of lists of bools), or [a]
(the polymorphic type of lists of a
); []
is the thing that's being applied to Int
, Bool
, and a
in those examples.
You can actually write [Int]
as [] Int
if you want, though it looks weird, so you usually only see []
at the type level when you want to use it unapplied.
Lets take a look at your data declaration again:
data Property f a = Property String (f a) | Zilch
On the left-hand side you've declared the shape of the type Property
; Property f a
forms a type. On the right hand side you declare the shape of the values that go in that type, by listing the possible value constructors (Property
and Zilch
) and the types of the "slots" in those constructors (none for Zilch
; one slot of type String
and another one of type f a
, for Property
).
So from that we can tell that whatever f
and a
are, the type expression f a
(f
applied to a
) must form a type that has values. But f
doesn't have to be (in fact it can't be) a normal type of values on its own! There is no slot of type f
in the Property
value constructor.
A much clearer example to use would have been this:
*Main> var = Property "Stuff" (Just True)
*Main> :t var
var :: Property Maybe Bool
If you don't know it, Maybe
is a built in type whose declaration looks like this:
data Maybe a = Just a | Nothing
It's good for this example because we're not using the same name at the type level and the value level, which avoids confusion when you're trying to learn how things work.
Just True
is a value of type Maybe Bool
. At the value level we have the Just
data constructor applied to the value True
. At the type level we have the Maybe
type constructor applied to the type Bool
. Maybe Bool
values go in the f a
slot of the Property
value constructor, which fits straightforwardly: f
is Maybe
and a
is Bool
.
So going back to your original example:
*Main> var = Property "Colors" [1,2,3,4]
*Main> :t var
var :: Num a => Property [] a
You're filling the f a
slot with [1, 2, 3, 4]
. That's a list of some kind of number, so it'll be Num t => [t]
. So the a
in f a
is the t
(with a Num
constraint that needs to come along), and the f
is the list type constructor []
. This []
is like Maybe
, not like Nothing
.
*Main> var = Property "Colors" (1,"Red")
*Main> :t var
var :: Num t => Property ((,) t) [Char]
Here the f a
slot is being filled with (1, "Red")
, which is of type Num t => (t, [Char])
(remembering that String
is just another way of writing [Char]
). Now to understand this we have to get a little finicky. Forget the constraint for now, and just focus on (t, [Char])
. Somehow we need to interpret that as something applied to something else, so we can match it to f a
. Well it turns out that although we have special syntax for tuple types (like (a, b)
), they're really just like ordinary ADTs you could declare without the special syntax. A 2-tuple type is a type constructor that we can write (,)
applied to two other types, in this case t
and [Char]
. And we can use partially applied type constructors, so we can think of (,)
applied to t
as one unit, and that unit applied to [Char]
. We can write that interpretation as a Haskell type expression ((,) t) [Char]
, but I'm not sure if that's clearer. But what it comes down to is that we can match this to f a
by taking the first "unit" (,) t
as f
and [Char]
as a
. Which then gives us Property ((,) t) [Char]
(only we have to also put back the Num t
constraint we forgot about earlier).
And finally this one:
*Main> var = Property "Colors" 20
*Main> :t var
var :: Num (f a) => Property f a
Here we're filling the f a
slot with 20
, some sort of number. We haven't specified exactly what type the number is, so Haskell is willing to believe it could be any type in the Num
class. But we still need the type to have a "shape" we can match with f a
: some type constructor applied to some other type. And it's the whole type expression f a
that needs to match the type of 20
, so that's what has a Num
constraint. But we haven't said anything else about what f
or a
might be, and 20
can by any type that meets a Num
constraint, so it can be any Num (f a) => f a
we want for it, hence why the type of your var
is still polymorphic in f
and a
(just with the added constraint).
You might have only seen numeric types like Integer
, Int
, Double
, etc, and so be wondering how there could possibly be an f a
that's a number; all of those examples are just single basic types, not something applied to something. But you can write your own Num
instances, so Haskell never assumes a given type (or shape of type) couldn't be a number, it'll just complain if you actually attempt to use it and it can't find a Num
instance. So sometimes you get things like this that are probably errors, but Haskell accepts (for now) with a Num
type on an odd thing that you weren't expecting.
And in fact there are already types in the built-in libraries that do have compound type-level structore and have a Num
instance. One example is the Ratio
type for representing fractional numbers as ratios of two integers. You can have a Ratio Int
or a Ratio Integer
, for example:
Main*> 4 :: Ratio Int
4 % 1
So you could say:
*Main> var = Property "Colors" (20 :: Ratio Integer)
*Main> :t var
var :: Property Ratio Integer
1 Actually there can be, with the DataKinds
extension enabled to allow types that mirror the structure of almost any value, so you can have type-level lists. But that's not what's going on here and it's not really a feature you can use until you've got a good handle on the way types and values work in vanilla Haskell, so I recommend you ignore this footnote and pretend it doesn't exist yet.
Property "Colors" (1,"Red")
, try:t (1,3) :: ((,) Int) Integer
at GHCi prompt. – Will Ness