[Haskell-beginners] fromIntegral
Brent Yorgey
byorgey at seas.upenn.edu
Sat Oct 2 17:43:56 EDT 2010
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 <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
> >
> >
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners
More information about the Beginners
mailing list