giving types for expressions

Question

So I'm being asked to "Give possible types (not involving any type variables) for each of the following expressions (or else explain why you think the expression is ill-typed)" and I'm struggling with the expression [ [], [[]], [[[]]], [[[[]]]], [[[[[ ]]]]] ].

When I put :t *the above expression* into ghci it tells me that it has the type [[[[[[a]]]]]]. I'm confused what the expression is even saying and why it's giving me that type.

Also :t [ [True], [[]], [[[]]], [[[[]]]], [[[[[]]]]] ] gives an error, and I don't know why it is ill typed. I think the answer to the first one will help me understand why the second expression fails.

Answer 1

You have the value [ [], [[]], [[[]]], [[[[]]]], [[[[[ ]]]]] ], which is a list of nested lists.

• The rightmost value is the most constrained: we know how deeply nested this list must be.
• The leftmost value is the least constrained: it is just an empty list, so it could be a list of anything.

If we apply the least constraining type to each of these, we get:

[
  [        ] -- [    a    ]
, [[      ]] -- [[   b   ]]
, [[[    ]]] -- [[[  c  ]]]
, [[[[  ]]]] -- [[[[ d ]]]]
, [[[[[]]]]] -- [[[[[e]]]]]
]

The list must have a homogenous type, so we look at unifying them. If we try to unify the first two types, [a] and [[b]], we see that a ⊇ [b], so we now have:

[
  [  ] -- [[b]]
, [[]] -- [[b]]
, ...
]

If we continue this process up to [[[[d]]]] and [[[[[e]]]]], we see that d ⊇ [e], and so we end up with:

[
  [        ] -- [[[[[e]]]]]
, [[      ]] -- [[[[[e]]]]]
, [[[    ]]] -- [[[[[e]]]]]
, [[[[  ]]]] -- [[[[[e]]]]]
, [[[[[]]]]] -- [[[[[e]]]]]
]

And so finally, the overall list has type [[[[[[e]]]]]].

This is because the first element is an empty list of whatever, the second is a single-element list with an empty list of whatever, and so on. You could repeat this process ad infinitum, with nested singleton lists ending at a single empty list, and your type would be [[...[a]...]].

So now that you know how many levels of nesting there must be before you can introduce your own type (by replacing e), you should be able to see why [ [True], [[]], [[[]]], [[[[]]]], [[[[[]]]]] ] is not valid, but [ [], [[]], [[[]]], [[[[]]]], [[[[[True]]]]] ] is.

Answer 2

To understand why the expression: [ [], [[]], [[[]]], [[[[]]]], [[[[[ ]]]]] ] has type [[[[[[a]]]]]], you need to understand what is the type of [] first.

Actually, [] is equivalent to [a'], where a' is type variable without any constraint. That means a' can be any type. So, when a list is constructed, say, [ [], [[]] ], it is legal to replace a' with [a] as:

[ [], [[]] ] ~ [ [a'] [[a]] ] ~ [ [[a]], [[a]] ] ~ [ [[a]] ]

The same reason why

[ [], [[]], [[[]]], [[[[]]]], [[[[[ ]]]]] ] ~  [ [[[[[a]]]]] ]

But when you constructs a list as [ [True], [[]] ], there is no way to convert True to a list, even though [a] can be any type of list. The same reason why [ [True], [[]], [[[]]], [[[[]]]], [[[[[]]]]] ] is illegal.