[Haskell-beginners] fromIntegral

[Daniel Fischer]

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