[Haskell-beginners] fromIntegral

[Russ Abbott]

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 at 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/beginners/attachments/20101002/b1d8590a/attachment-0001.html