Daniel, I appreciate your help. Let me tell you where I'm coming from. I teach an introductory Haskell course once a year. I'm not a Haskell expert, and I tend to forget much of what I knew from one year to the next. Perhaps more importantly, one reason for asking these questions is to explain what's going on to students who are just seeing Haskell for the first time. We are now 2 weeks into the course. If this can't be explained (at least at an intuitive level) without displaying lots of intermediate code, it doesn't help me.

So here are a couple of questions about this example.

What does it mean to say a Num instance for Char. Can you give me an example of what that means in a program that will execute. (Preferably the program would be as simple as possible.)

Is there a way to display a value along with its type during program execution? I know about Show; is there something similar like ShowWithType (or even ShowType) that (if implemented) will generate a string of a value along with its type?

It makes sense to me to say that [ ] is a function that takes a type as an argument and generates an value. If that's the case, it also makes sense to say that [ ] == [ ] can't be evaluated because there is simply no == for functions.

It also makes sense to me to say that == is a collection of more concrete functions from which one is selected depending on the type required by the expression within which == appears.

Since the required type is known at compile time, it would seem that the selection of which == to use could be made at compile time. One shouldn't have to carry along a dictionary. (Perhaps someone said that earlier. But if so, why the long discussion about Dictionaries?) This seems like a standard definition of an overloaded function. So why is there an objection to simply saying that == is overloaded and letting it go at that?

The answer to why tail ['a'] == [ ] is ok would go something like this. (Is this ok?)

a. [ ] is a function that takes a type argument and generates the empty list of that type. In particular [ ] is not a primitive value.

b. The type of the lhs is [Char].

c. That selects == :: [Char] -> [Char] -> Bool as the version of == to use in the expression.

d. That inserts Char as the Type argument to be passed to the [ ] function on the rhs.

e. All the preceding can be done at compile time.

f. When executed, the lhs and rhs will both execute the [ ] function with argument Char. They both generate the value [ ] :: [Char]. Those two values will be identical and the value of the expression will be True.

The reason == at the Equ level appears not to be transitive is that the "middle" element is not the same. We can write

let xs = []
ys = 1:xs
zs = 'a': xs
in tail ys == xs && xs == tail zs

But that doesn't imply that tail ys == tail zs. The reason is that in the left expression xs is the [ ] function that is passed Char, and in the right expression xs is the [ ] function that is passed Int. Since xs does not refer to the same thing in both places, transitivity is not violated.

In other words, xs is something like (f Char) on the left and (f Int) on the right--where f is the [ ] function. There is no reason to expect that (f Char) == (f Int). That expression is not even valid because the left and right types are different.

All of the preceding is something I would feel comfortable saying to someone who is just 2 weeks into Haskell. There may be a lot of pieces to that explanation, but none of them require much prerequisite Haskell knowledge.

-- Russ

On Sat, Oct 2, 2010 at 7:09 AM, Daniel Fischer <daniel.is.fischer@web.de> wrote:

On Saturday 02 October 2010 07:24:38, Russ Abbott wrote:
> Thanks. I'm still wondering what [ ] refers to.

That depends where it appears. Leaving aside []'s existence as a type
constructor, it can refer to
- an empty list of specific type
- an empty list of some constrained type (say, [] :: Num a => [a])
- an empty list of arbitrary type.

At any point where it is finally used (from main or at the interactive
prompt), it will be instantiated at a specific type (at least in GHC).

At the Haskell source code level, [] is an expression that can have any
type [a].

At the Core level (first intermediate representation in GHC's compilation
process, still quite similar to Haskell), [] is a function which takes a
type ty as argument and produces a value of type [ty].

At the assembly level, there are no types anymore, and I wouldn't be
surprised if all occurrences of [] compiled down to the same bit of data.

> I can load the following file without error.
>
> null' xs = xs == [ ]

Let's see what Core the compiler produces of that:

Null.null' :: forall a_adg.
(GHC.Classes.Eq a_adg) =>
[a_adg] -> GHC.Bool.Bool

--Straightforward, except perhaps the name mangling to produce unique
names.

GblId
[Arity 1]

--Lives at the top level and takes one argument.

Null.null' =
\ (@ a_ahp) ($dEq3_aht :: GHC.Classes.Eq a_ahp) ->

--Here it gets interesting, at this level, it takes more than one argument,
the first two are given here, a type a_ahp, indicated by the @ [read it as
"null' at the type a_ahp] and an Eq dictionary for that type.

let {
==_ahs :: [a_ahp] -> [a_ahp] -> GHC.Bool.Bool

--Now we pull the comparison function to use out of the dictionary and bind
it to a local name.

LclId
[]
==_ahs =
GHC.Classes.== @ [a_ahp] (GHC.Base.$fEq[] @ a_ahp $dEq3_aht) } in

--First, from the Eq dictionary for a_ahp, we pull out the Eq dictionary
for the type [a_ahp] and from that we choose the "==" function.

\ (xs_adh :: [a_ahp]) -> ==_ahs xs_adh (GHC.Types.[] @ a_ahp)

--And now we come to the point what happens when the thing is called.
Given an argument xs_adh of type [a_ahp], it applies the comparison
function pulled out of the dictionary(ies) to a) that argument and b) []
(applied to the type a_ahp, so as the value [] :: [a_ahp]).

>
> test =
> let x = [ ]
> in tail [1] == x && tail ['a'] == x

And here (caution, it's long and complicated, the core you get with
optimisations is much better),

$dEq_riE :: GHC.Classes.Eq [GHC.Types.Char]
GblId
[]
$dEq_riE = GHC.Base.$fEq[] @ GHC.Types.Char GHC.Base.$fEqChar

-- The Eq dictionary for [Char], pulled from the Eq dictionary for Char

$dEq1_riG :: GHC.Classes.Eq GHC.Integer.Type.Integer
GblId
[]
$dEq1_riG =
GHC.Num.$p1Num @ GHC.Integer.Type.Integer GHC.Num.$fNumInteger

-- The Eq dictionary for Integer, pulled from the Num dictionary for
Integer (Eq is a superclass of Num, so the Num dictionary contains [a
reference to] the Eq dictionary)

$dEq2_riI :: GHC.Classes.Eq [GHC.Integer.Type.Integer]
GblId
[]
$dEq2_riI = GHC.Base.$fEq[] @ GHC.Integer.Type.Integer $dEq1_riG

-- The Eq dictionary for [Integer] pulled from the Eq dictionary for
Integer

Null.test :: GHC.Bool.Bool
GblId
[]
Null.test =
GHC.Classes.&&
(GHC.Classes.==
@ [GHC.Integer.Type.Integer]
$dEq2_riI

-- pull the "==" member from the Eq dictionary for [Integer]

(GHC.List.tail
@ GHC.Integer.Type.Integer

-- apply tail to a list of Integers

(GHC.Types.:
@ GHC.Integer.Type.Integer

-- cons (:) an Integer to a list of Integers

(GHC.Integer.smallInteger 1)

-- 1

(GHC.Types.[] @ GHC.Integer.Type.Integer)))

-- empty list of integers, first arg of == complete.

(GHC.Types.[] @ GHC.Integer.Type.Integer))

-- empty list of Integers, second arg of ==, completes first arg of &&

(GHC.Classes.==
@ [GHC.Types.Char]
$dEq_riE

-- pull the == function from the Eq dictionary for [Char]

(GHC.List.tail
@ GHC.Types.Char

-- apply tail to a list of Chars

(GHC.Types.:
@ GHC.Types.Char

-- cons a Char to a list of Chars

(GHC.Types.C# 'a')

-- 'a'

(GHC.Types.[] @ GHC.Types.Char)))

-- empty list of Chars, first arg of == complete

(GHC.Types.[] @ GHC.Types.Char))

-- empty list of Chars, second arg of ==, completes second arg of &&

When compiled with optimisations, a lot of the stuff is done at compile
time and we get the more concise core

Null.test :: GHC.Bool.Bool
GblId
[Str: DmdType]
Null.test =
case GHC.Base.$fEq[]_==
@ GHC.Integer.Type.Integer
GHC.Num.$fEqInteger
(GHC.Types.[] @ GHC.Integer.Type.Integer)
(GHC.Types.[] @ GHC.Integer.Type.Integer)
of _ {
GHC.Bool.False -> GHC.Bool.False;
GHC.Bool.True ->
GHC.Base.eqString
(GHC.Types.[] @ GHC.Types.Char) (GHC.Types.[] @ GHC.Types.Char)
}

The tails are computed at compile time and the relevant dictionaries are no
longer looked up in the global instances table but are directly referenced.

>
> (I know I can define null' differently. I'm defining it this way so that
> I can ask this question.)
>
> When I execute test I get True.
> > test
> True
>
> So my question is: what is x after compilation? Is it really a thing of
> type
>
> (Eq a) => [a] ?

During compilation, the types at which x is used are determined (for the
first list, the overloaded type of 1 :: Num a => a is defaulted to Integer,
hence we use [] as an empty list of Integers, the second type is explicit)
and the (hidden, not present at source level) type argument is filled in,
yielding a value of fixed type. x is used at two different types, so we get
two different (at Core level) values.

Since x is local to test, x doesn't exist after compilation.
It would still exist if it was defined at the module's top level and was
exported.

> If so, how should I think of such a thing being stored so that it can be
> found equal to both tail [1] and tail ['a']?

Perhaps it's best to think of a polymorphic expression as a function taking
types (one or more) as arguments and returning a value (of some type
determined by its type arguments; that value can still be a function taking
type arguments if fewer type arguments are provided than the expression
takes).

> Furthermore, this seems to
> show that (==) is not transitive

At any specific type, (==) is (at least it should be) transitive, but you
can't compare values of different types.

> since one can't even compile
> tail [1] == tail ['a']

Type error, of course, on the right, you have a value of type [Char], on
the left one of Type Num n => [n].
If you povide a Num instance for Char, it will complie and work.

> much less find them to be equal. Yet they are each == to x.

Yes, x can have many types, it's polymorphic.

>
> -- Russ