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