On Fri, Oct 1, 2010 at 12:08 PM, Russ Abbott wrote: ] ] On Thu, Sep 30, 2010 at 10:25 PM, Felipe Lessa ] wrote: ]] Now, maybe 'fromIntegral' has something more than polymorphism? ]] Well, it has typeclasses.  But we can represent those as ]] data types, so we could write ]] ]]  fromIntegralD :: Integral a -> Num b -> a -> b ]]  fromIntegralD intrDictA numDictB = ]]    fromIntegral numDictB . toInteger intrDictA ] ] I'm afraid I don't understand this. Moreover, I couldn't get the preceding ] to load without error. Let's simplify things a little bit to make a runnable example. Suppose we have

class MonoidClass a where mc_empty :: a mc_append :: a -> a -> a

We can construct the following function:

mc_concat :: MonoidClass a => [a] -> a mc_concat [] = mc_empty mc_concat (x:xs) = mc_append x (mc_concat xs)

Pretty standard stuff. Now, the 'MonoidClass' class could also be a plain data type:

data MonoidDict a = MD {md_empty :: a ,md_append :: a -> a -> a}

I have just put the members of the class as fields of a data type. Now 'mc_concat' can be written as:

md_concat :: MonoidDict a -> [a] -> a md_concat md [] = md_empty md md_concat md (x:xs) = md_append md x (md_concat md xs)

So, while 'mc_concat' has constraints, 'md_concat' is just as pure polymorphic as 'length' is. ]] Functions that are polymorphic but do not have constraints are ]] not really overloaded because of parametricity, which means that ]] they can't change the way they work based on the specific choices ]] of types you make. ] ] I don't understand the preceding paragraph. Would you mind elaborating. Take 'length', for example. It has type length :: [a] -> Int As it is polymorphic on the list's element type, it can't behave any differently when I use it on an [Int] from when I use it on a [Double]. ]] > If so, can I say the same sort of thing about constants like 1 and []? ]] > In ]] > particular there is no single value []. Instead [] is a symbol which at ]] > compile time must be compiled to the empty list of some particular type, ]] > e.g., [Int].  There is no such Haskell value as [] :: [a] since [a] (as ]] > type) is not an actual type. I want to say the same thing about 1, i.e., ]] > that there is no such Haskell value as 1 :: (Num t) => t. When the ]] > symbol 1 ]] > appears in a program, the compiler must decide during compilation ]] > whether it ]] > is intended to be 1::Int or 1::Integer or 1::Double, etc. ]] ]] Well, [a] *is* an actual type, a polymorphic one. ] ] Here is the example that raised that issue for me. Let's say I define null' ] as follows. ] ]    null' xs = xs == [ ] ] ] If I don't include a declaration in the file, Haskell (reasonably) concludes ] the following. ] ]   > :t null' ]   null' :: (Eq a) => [a] -> Bool ] ] If I write the following at the top level, everything is fine. ]   > null' [ ] ]   True ] ] But if I include the following in the file that defines null', I get an ] error message. ] ]   test = null' [ ] ] ]       Ambiguous type variable `a' in the constraint: ]            `Eq a' arising from a use of `null'' at null.hs:6:17-24 ]          Probable fix: add a type signature that fixes these type ] variable(s) ] ] Why is that? And how can it be fixed?  I know I can fix it as follows. If your function was, for example,

null'' :: [a] -> Bool null'' [] = True null'' _ = False

then there would be no error. I assume you already figured that out. null'' works because it doesn't need to know what kind of list is. By parametricity, its behaviour can't change based on its type. However, null' *can* change its behaviour based on the elements type! It can use any of the functions in Eq class. For example,

nullW :: Eq a => [a] -> Bool nullW [x,y] = x == y nullW _ = False

Note that this functions has the same type as your null', however its behaviour depends on which kind of 'a' you give to it, as different 'a's have different (==)s. Another way of seeing this is by passing the type class as an argument (I'll omit /=):

data EqDict a = EQ {eq_equals :: a -> a -> Bool}

-- Takes equality for 'a' and returns equality for '[a]'. -- Just like the type class which is -- -- instance Eq a => Eq [a] where ... listEqDict :: EqDict a -> EqDict [a] listEqDict eq = EQ equals where equals [] [] = True equals (x:xs) (y:ys) = eq_equals eq x y && equals xs ys equals _ _ = False

nullDict :: EqDict a -> [a] -> Bool nullDict eq xs = eq_equals (listEqDict eq) xs []

So while null'' only takes the list as argument, nullDict also needs to know which EqDict you want to use. With type classes, this EqDict is chosen based on 'a's type. And that's precisely what the error message says. It says that type 'a' is ambigous because of the 'Eq a' constraint. ] It seemed to me that similar reasoning applied to things like 1.  How is the ] following explained? ] ]    Prelude> 111111111111111111111111111111111111111111 ]    111111111111111111111111111111111111111111 ]    it :: (Num t) => t ]    Prelude> maxBound :: Int ]    2147483647 ]    it :: Int ]    Prelude> 111111111111111111111111111111111111111111 - (1::Int) ]    -954437178 ]    it :: Int ] ] Does it make sense to say that the long string of 1's is really of type (Num ] t) => t? ] ] If so, what does the compiler think it's doing when it processes(?) it as an ] Int so that it can subtract 1 :: Int from it?  It didn't treat it as ] maxBound :: Int.  And yet it didn't generate an error message. This is the same thing. The type (Num t) => t really is the same as NumDict t -> t Hope that helps, =) -- Felipe.

Thanks. I'm still wondering what [ ] refers to. I can load the following file without error. null' xs = xs == [ ] test = let x = [ ] in tail [1] == x && tail ['a'] == x (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] ? 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']? Furthermore, this seems to show that (==) is not transitive since one can't even compile tail [1] == tail ['a'] much less find them to be equal. Yet they are each == to x. -- Russ On Fri, Oct 1, 2010 at 9:08 AM, Daniel Fischer wrote:

On Friday 01 October 2010 17:08:08, Russ Abbott wrote:

...

Thanks, Filipe

I clearly over-stated my case. I'd like to break it into a number of different question. Please see below.

On Thu, Sep 30, 2010 at 10:25 PM, Felipe Lessa wrote:

...

I'll try to clarify some concepts. Please correct me if I am wrong, and please forgive me if I misunderstood you.

On Fri, Oct 1, 2010 at 12:54 AM, Russ Abbott

wrote:

...

In explaining fromIntegral, I want to say that it is really a collection

of

...

overloaded functions:

Integer -> Double Int -> Float ...

When GHC compiles a line of code with fromIntegral it in, it must decide

at

...

compile time which of these overloaded functions to compile to. This is

in

...

contrast to saying that fromIngetral is a function of the type (Integral

a,

...

Num b) => a -> b. In reality there is no (single) function of the type (Integral a, Num b) => a -> b because (among other things) every function must map between actual types, but (Integral a, Num b) => a -> b does not say which actual types are mapped between.

Is the preceding a reasonable thing to say?

First of all, I do think that polymorphic functions are plain ol' functions. For example

id :: a -> a id x = x

is a function. Moreover, in GHC 'id' has only one representation, taking a thunk and returning a thunk, so even at the machine code level this is only one function.

Agree. I over stated my case. The same can be said for length :: [a] -> Int It doesn't matter what the type of element in the list is. length runs the same way no matter what. So this is pure polymorphism.

...

Now, maybe 'fromIntegral' has something more than polymorphism? Well, it has typeclasses. But we can represent those as data types, so we could write

fromIntegralD :: Integral a -> Num b -> a -> b fromIntegralD intrDictA numDictB = fromIntegral numDictB . toInteger intrDictA

I'm afraid I don't understand this. Moreover, I couldn't get the preceding to load without error.

No wonder, Integral and Num are type classes and not datatypes (unless you have defined such datatypes in scope).

The point is, you can represent type classes as dictionaries, e.g.

data Num a = NumDict { plus :: a -> a -> a , minus :: a -> a -> a , ... , fromIntegerD :: Integer -> a }

data Integral a = IntegralDict { quotD :: a -> a -> a , ... , toIntegerD a }

Then a type-class polymorphic function like fromIntegral becomes a function with some dictionaries as additional arguments.

foo :: (Class1 a, Class2 b) => a -> b

becomes

fooDict :: Class1Dict a -> Class2Dict b -> a -> b

To do that explicitly is of course somewhat cumbersome as one has to always carry the dictionaries around and one can have more than one dictionary per type (e.g.

intNum1 :: Num Int intNum1 = NumDict { plus = (+) , ... , fromIntegerD = fromInteger }

intNum2 :: Num Int intNum2 = NumDict { plus = quot , -- more nonsense , fromInteger = const 1 } ).

Internally, GHC implements type classes via dictionaries and passes them as extra arguments to overloaded functions, as you can see by inspecting the Core output (-ddump-simpl).

...

...

Better yet, the compiler could write this code for us internally.

And GHC does.

...

...

Now, using thunks we can get a single machine code for 'fromIntegralD' as well.

But that's not terribly efficient, so with -O, GHC tries to eliminate dictionaries and use the specialised functions (like plusInteger :: Integer -> Integer -> Integer).

...

...

In sum, I think all functions are really just that, functions.

--

You may call functions that have typeclass constraints "overloaded functions", but they still are functions.

Functions that are polymorphic but do not have constraints are not really overloaded because of parametricity, which means that they can't change the way they work based on the specific choices of types you make.

I don't understand the preceding paragraph. Would you mind elaborating.

For a function like

length :: [a] -> Int

, because it doesn't know anything about the type a at which it will be called, it cannot do anything with the contents of the list (well, it could call seq on them, but it would do that for every type), it can only inspect the spine of the list.

The code is completely independent of what type of data the pointers to the contents point to, so `length [True,False]' and `length [()]' can and do call the exact same machine code.

...

...

...

If so, can I say the same sort of thing about constants like 1 and []? In particular there is no single value []. Instead [] is a symbol which at compile time must be compiled to the empty list of some particular type, e.g., [Int]. There is no such Haskell value as [] :: [a] since [a] (as type) is not an actual type. I want to say the same thing about 1, i.e., that there is no such Haskell value as 1 :: (Num t) => t. When the symbol

1

...

appears in a program, the compiler must decide during compilation whether

it

...

is intended to be 1::Int or 1::Integer or 1::Double, etc.

Well, [a] *is* an actual type, a polymorphic one.

Here is the example that raised that issue for me. Let's say I define null' as follows.

null' xs = xs == [ ]

If I don't include a declaration in the file, Haskell (reasonably) concludes the following.

...

:t null'

null' :: (Eq a) => [a] -> Bool

If I write the following at the top level,

You seem to mean the ghci prompt here, not the top level of a module.

...

everything is fine.

...

null' [ ]

True

But if I include the following in the file that defines null', I get an error message.

test = null' [ ]

Ambiguous type variable `a' in the constraint: `Eq a' arising from a use of `null'' at null.hs:6:17-24 Probable fix: add a type signature that fixes these type variable(s)

Why is that?

null' has an Eq constraint, so to evaluate test, an Eq dictionary is needed, but there's no way to determine which one should be used.

At a lower level, the type of null' is

null' :: EqDict a -> [a] -> Bool

The (hidden) first argument is missing and GHC doesn't know which one to pass.

At the ghci-prompt, ghci's extended default rules let it selet the Eq dictionary of () and all's fine.

In a source file, GHC restricts itself to the default rules specified in the language report, which state that for defaulting to take place, at least one of the constraints must be a numeric class. There's none here, so no defaulting and the type variable of the constraint remains ambiguous.

...

And how can it be fixed? I know I can fix it as follows.

test = null' ([ ] :: [Integer])

...

:reload

test

True

In that situation, I think giving a type signature is the only way¹.

test = null' ([] :: Num a => [a])

also works.

¹ -XExtendedDefaultRules might work too.

...

That's what suggested to me that [ ] had to be compiled into a concrete value.

Try

null'' [] = True null'' _ = False

test'' = null'' []

No type class constraints, no problems.

...

It seemed to me that similar reasoning applied to things like 1. How is the following explained?

Prelude> 111111111111111111111111111111111111111111 111111111111111111111111111111111111111111 it :: (Num t) => t Prelude> maxBound :: Int 2147483647 it :: Int Prelude> 111111111111111111111111111111111111111111 - (1::Int) -954437178 it :: Int

Does it make sense to say that the long string of 1's is really of type (Num t) => t?

Integer literals stand for (fromInteger Integer-value-of-literal), so the literal itself can have any type belonging to Num. If you force it to have a particular type, the corresponding fromInteger function is determined and can be applied if the value is needed.

...

If so, what does the compiler think it's doing when it processes(?) it as an Int so that it can subtract 1 :: Int from it? It didn't treat it as maxBound :: Int. And yet it didn't generate an error message.

For efficiency, fromInteger wraps, for a b-bit Integral type, the result of fromInteger n is n `mod` 2^b.

...

Thanks

-- Russ

It turns out that test1 = 1 == 1 will load (and return True), but testNull = [ ] == [ ] won't load. Both 1 and [ ] seem to have similar sorts of type parameters in their types. Why are they treated differently? -- Russ On Fri, Oct 1, 2010 at 10:40 PM, Russ Abbott wrote:

I can even write

test = let x = [] y = 1 : x z = 'a' : x in ...

But clearly I can't write tail y == tail z. Does that imply that type inferencing prevents one from writing a True expression?

-- Russ

On Fri, Oct 1, 2010 at 10:24 PM, Russ Abbott wrote:

...

Thanks. I'm still wondering what [ ] refers to. I can load the following file without error.

null' xs = xs == [ ]

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

(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] ? 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']? Furthermore, this seems to show that (==) is not transitive since one can't even compile tail [1] == tail ['a'] much less find them to be equal. Yet they are each == to x.

-- Russ

On Fri, Oct 1, 2010 at 9:08 AM, Daniel Fischer wrote:

...

On Friday 01 October 2010 17:08:08, Russ Abbott wrote:

...

Thanks, Filipe

I clearly over-stated my case. I'd like to break it into a number of different question. Please see below.

On Thu, Sep 30, 2010 at 10:25 PM, Felipe Lessa wrote:

...

I'll try to clarify some concepts. Please correct me if I am wrong, and please forgive me if I misunderstood you.

On Fri, Oct 1, 2010 at 12:54 AM, Russ Abbott

wrote:

...

In explaining fromIntegral, I want to say that it is really a collection

of

...

overloaded functions:

Integer -> Double Int -> Float ...

When GHC compiles a line of code with fromIntegral it in, it must decide

at

...

compile time which of these overloaded functions to compile to. This is

in

...

contrast to saying that fromIngetral is a function of the type (Integral

a,

...

Num b) => a -> b. In reality there is no (single) function of the type (Integral a, Num b) => a -> b because (among other things) every function must map between actual types, but (Integral a, Num b) => a -> b does not say which actual types are mapped between.

Is the preceding a reasonable thing to say?

First of all, I do think that polymorphic functions are plain ol' functions. For example

id :: a -> a id x = x

is a function. Moreover, in GHC 'id' has only one representation, taking a thunk and returning a thunk, so even at the machine code level this is only one function.

Agree. I over stated my case. The same can be said for length :: [a] -> Int It doesn't matter what the type of element in the list is. length runs the same way no matter what. So this is pure polymorphism.

...

Now, maybe 'fromIntegral' has something more than polymorphism? Well, it has typeclasses. But we can represent those as data types, so we could write

fromIntegralD :: Integral a -> Num b -> a -> b fromIntegralD intrDictA numDictB = fromIntegral numDictB . toInteger intrDictA

I'm afraid I don't understand this. Moreover, I couldn't get the preceding to load without error.

No wonder, Integral and Num are type classes and not datatypes (unless you have defined such datatypes in scope).

The point is, you can represent type classes as dictionaries, e.g.

data Num a = NumDict { plus :: a -> a -> a , minus :: a -> a -> a , ... , fromIntegerD :: Integer -> a }

data Integral a = IntegralDict { quotD :: a -> a -> a , ... , toIntegerD a }

Then a type-class polymorphic function like fromIntegral becomes a function with some dictionaries as additional arguments.

foo :: (Class1 a, Class2 b) => a -> b

becomes

fooDict :: Class1Dict a -> Class2Dict b -> a -> b

To do that explicitly is of course somewhat cumbersome as one has to always carry the dictionaries around and one can have more than one dictionary per type (e.g.

intNum1 :: Num Int intNum1 = NumDict { plus = (+) , ... , fromIntegerD = fromInteger }

intNum2 :: Num Int intNum2 = NumDict { plus = quot , -- more nonsense , fromInteger = const 1 } ).

Internally, GHC implements type classes via dictionaries and passes them as extra arguments to overloaded functions, as you can see by inspecting the Core output (-ddump-simpl).

...

...

Better yet, the compiler could write this code for us internally.

And GHC does.

...

...

Now, using thunks we can get a single machine code for 'fromIntegralD' as well.

But that's not terribly efficient, so with -O, GHC tries to eliminate dictionaries and use the specialised functions (like plusInteger :: Integer -> Integer -> Integer).

...

...

In sum, I think all functions are really just that, functions.

--

You may call functions that have typeclass constraints "overloaded functions", but they still are functions.

Functions that are polymorphic but do not have constraints are not really overloaded because of parametricity, which means that they can't change the way they work based on the specific choices of types you make.

I don't understand the preceding paragraph. Would you mind elaborating.

For a function like

length :: [a] -> Int

, because it doesn't know anything about the type a at which it will be called, it cannot do anything with the contents of the list (well, it could call seq on them, but it would do that for every type), it can only inspect the spine of the list.

The code is completely independent of what type of data the pointers to the contents point to, so `length [True,False]' and `length [()]' can and do call the exact same machine code.

...

...

...

If so, can I say the same sort of thing about constants like 1 and []? In particular there is no single value []. Instead [] is a symbol which at compile time must be compiled to the empty list of some particular type, e.g., [Int]. There is no such Haskell value as [] :: [a] since [a] (as type) is not an actual type. I want to say the same thing about 1, i.e., that there is no such Haskell value as 1 :: (Num t) => t. When the symbol

1

...

appears in a program, the compiler must decide during compilation whether

it

...

is intended to be 1::Int or 1::Integer or 1::Double, etc.

Well, [a] *is* an actual type, a polymorphic one.

Here is the example that raised that issue for me. Let's say I define null' as follows.

null' xs = xs == [ ]

If I don't include a declaration in the file, Haskell (reasonably) concludes the following.

...

:t null'

null' :: (Eq a) => [a] -> Bool

If I write the following at the top level,

You seem to mean the ghci prompt here, not the top level of a module.

...

everything is fine.

...

null' [ ]

True

But if I include the following in the file that defines null', I get an error message.

test = null' [ ]

Ambiguous type variable `a' in the constraint: `Eq a' arising from a use of `null'' at null.hs:6:17-24 Probable fix: add a type signature that fixes these type variable(s)

Why is that?

null' has an Eq constraint, so to evaluate test, an Eq dictionary is needed, but there's no way to determine which one should be used.

At a lower level, the type of null' is

null' :: EqDict a -> [a] -> Bool

The (hidden) first argument is missing and GHC doesn't know which one to pass.

At the ghci-prompt, ghci's extended default rules let it selet the Eq dictionary of () and all's fine.

In a source file, GHC restricts itself to the default rules specified in the language report, which state that for defaulting to take place, at least one of the constraints must be a numeric class. There's none here, so no defaulting and the type variable of the constraint remains ambiguous.

...

And how can it be fixed? I know I can fix it as follows.

test = null' ([ ] :: [Integer])

...

:reload

test

True

In that situation, I think giving a type signature is the only way¹.

test = null' ([] :: Num a => [a])

also works.

¹ -XExtendedDefaultRules might work too.

...

That's what suggested to me that [ ] had to be compiled into a concrete value.

Try

null'' [] = True null'' _ = False

test'' = null'' []

No type class constraints, no problems.

...

It seemed to me that similar reasoning applied to things like 1. How

is

...

the following explained?

Prelude> 111111111111111111111111111111111111111111 111111111111111111111111111111111111111111 it :: (Num t) => t Prelude> maxBound :: Int 2147483647 it :: Int Prelude> 111111111111111111111111111111111111111111 - (1::Int) -954437178 it :: Int

Does it make sense to say that the long string of 1's is really of type (Num t) => t?

Integer literals stand for (fromInteger Integer-value-of-literal), so the literal itself can have any type belonging to Num. If you force it to have a particular type, the corresponding fromInteger function is determined and can be applied if the value is needed.

...

If so, what does the compiler think it's doing when it processes(?) it as an Int so that it can subtract 1 :: Int from it? It didn't treat it as maxBound :: Int. And yet it didn't generate an error message.

For efficiency, fromInteger wraps, for a b-bit Integral type, the result of fromInteger n is n `mod` 2^b.

...

Thanks

-- Russ

On Saturday 02 October 2010 07:40:19, Russ Abbott wrote:

I can even write

test =    let x = []        y = 1 : x        z = 'a' : x    in ...

But clearly I can't write tail y == tail z.  Does that imply that type inferencing prevents one from writing a True expression?

Since it's not a well typed expression (unless there's a Num instance for Char in scope, in which case it would work), it doesn't have a value, in particular it's not a True expression. Haskell allows you only to write well typed expressions.

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 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

On Saturday 02 October 2010 23:28:59, Thomas wrote:

So, instantiating Char for Num would require you to provide implementations for (+), (*), (-), negate, abs, signum and fromInteger for Char. While syntactically possible, I don't see any semantically reasonable way to do so.

For some values of reasonable, defining the operations via the Enum instance is semantically reasonable. It's however not the best approach, even if for some odd reason you need 21-bit integers.

...

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?

AFAIK in GHCi you can do both, but not simultaneously: Prelude> let a = 5::Int Prelude> :t a a :: Int Prelude> a 5

:set +t makes ghci display the type of an expression entered at the prompt (except if it's an IO-action, then it behaves a little different).

...

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.

Prelude> :t [] [] :: [a]

So [] is a list type, not a function type.

Right. [] as a function taking a type as argument is how it's represented at the Core level in GHC, not how it's understood at the Haskell level or the assembly level.

Prelude> [] == [] True

You can actually compare [] to itself.

At the ghci prompt, since that uses extended default rules and chooses to compare at the type [()]. In a source file, you'd have to turn on the extended default rules ({-# LANGUAGE ExtendedDefaultRules #-}) or tell the compiler which type to use.

So your reasoning does not seem to be valid to me. At least not on the Haskell source code level (which is what you and your students work with). Daniel referred to the Core level when saying that [] was a function there.

My reasoning would go somewhere along the following line: [] has a polymorphic type, specifically it's an empty list of elements of any type ([] :: [a], type variable a is not restricted)

So, [] will compare to any empty list, no matter what its elements' type actually is.

You need an Eq instance, of course.

Given:

...

let xs = [] ys = 1:xs zs = 'a': xs

Then "tail ys == tail zs" will not type check. Neither "tail ys" nor "tail zs" are polymorphic: ys :: [Integer]

Well, tail ys is polymorphic, its type is tail ys :: Num a => [a] the type variable a is defaulted to Integer if there are no further constraints on a. If you use it for other stuff, it can be used at other types too. Prelude> let xs = []; ys = 1:xs; ws = length xs:tail ys; vs = pi:tail ys in (tail ws, tail vs) ([],[]) it :: (Floating a) => ([Int], [a])

zs :: [Char]

So the expression "tail ys == tail zs" is invalid - the lhs and rhs must have the same type but they do not. Nothing will get compared, no tail will be determined - it will just plainly be rejected from the compiler (or interpreter).

For comparison: "tail ys == []" is different. (tail ys) :: [Integer] [] :: [a]

So we set (well, GHC does this for us) type variable a to Integer and have: tail ys :: [Integer] == [] :: [Integer] which is perfectly valid.

Yep.

...

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.

See above - [] is not a function.

...

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?

(==) :: (Eq a) => a -> a -> Bool

So, yes, (==) feels a little like an overloaded function.

And such functions are often called overloaded.

It is a function that accepts any Eq-comparable type. However, overloading IIRC does not behave identically.

Overloading in Java, C# etc. behaves differently. Overloading is still a good term to describe (==) etc. in my opinion. One has to be aware that the word denotes different though related concepts for different languages, of course.

For example function arity is not required to be the same when overloading methods - and restrictions on types are very different, too.

HTH, Thomas

A meta-comment: you seem to be quite hung up on what something like [] actually *is*. While this is a valid question, it is complicated by the fact that the answer is different depending on the level at which you consider it. For example, at the surface language level, [] is a value with the polymorphic type [a]. At the core language level, it is actually a function which takes a type T as an argument and produces a value of type [T]. And at the runtime level, it is a certain bit-pattern which is going to be the same bit-pattern no matter what the type of the list. -Brent On Sat, Oct 02, 2010 at 12:53:11PM -0700, Russ Abbott wrote:

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 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

_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

Perhaps it's best to say that for the time being, they should regard polymorphic expressions like [] as either one symbol denoting different values of different types or one value having many types, whichever they feel more comfortable with.

I would like to be able to say that [ ] is one symbol denoting different values of different types and that the compiler picks which value it denotes given the context. But the example program disallows that--which is how I came up with the example in the first place. let xs = [] ys = 1:xs zs = 'a': xs in ... xs is not bound to a value with a concrete type (like [Int] or [Char]) at compile time. Even after compilation xs :: [a]. To say that [ ] is a value having many different types seems to be saying more or less the same thing, namely that compilation doesn't pick a particular concrete type. So what are the other options? I still like the idea of saying that [ ] is a function that takes a type as an argument and generates a value. (I believe this was your explanation at one point.) I realize that it isn't a function at the Haskell level. But it makes intuitive sense to say that the compiler generates such a function, which is what is bound to xs. It is that function that gets executed when the program is run. I know that for optimization purposes it may be compiled down past that interpretation and I also know that this function isn't a Haskell function. But if one were giving an operational semantics for what's going on (which I guess is what the Core effectively is) that seems to be the most transparent explanation.