On Friday 29 July 2011, 03:26:33, Jake Penton wrote:

Ok, thanks. I have some studying to do about haskell types, clearly.

Does that mean then that there is no definition possible of f other than 'undefined'? I mean this compiles:

f::a f = undefined

But is there any other possible second line defining f?

Sure, you can write the same thing in many different ways: f :: a f = f f :: a f = let x = x in x f :: a f = error "Foo" but all definitions of "f :: a" that compile yield (some kind of) bottom, since _|_ is the only value that is common to all types (whether an attempt to evaluate such a value yields actual nontermination or an exception message depends; the first two don't terminate in ghci but result in "<<loop>>" when used in a compiled programme).

- Jake -

Well, thanks everyone. I'm getting there slowly. I have had less success learning Haskell by just using it than any other language I have tackled. I seem to need to cycle regularly between some theoretical study and practical use. Actually, starting in September I shall be taking a grad course on languages. The text is Types and Programming Languages by Pierce. I looked quickly at the book after posting my question, and believe that the course will plug some major gaps in my understanding of types. - Jake -

On 2011-07-29, at 6:54 AM, Gary Klindt wrote:

So, why is it possible to work with the map :: (a -> b) -> [a] -> [b] function? One can use it with list of number and functions on numbers, can't one.

Yeah. Your question is pretty much an example of what what troubling me in my original post. And frankly, I doubt that my reasoning on this will get straightened out until I have studied the type system more thoroughly. Naively, the difference I see between your example using map and my original post is that I was *defining* f: f::a f = 1 which, I suppose, is quite a bit different than *calling* map. To parallel my example, one would (mistakenly) write something like this: map::(a -> b) -> [a] -> [b] map f lst = ['a','b','c'] The above gives the same message I got. It is tempting to think that " ['a','b','c'] is a list of b's, so it should work", but that is clearly wrong. - j -

On 2011-07-29, at 9:23 AM, James Cook wrote:

On Jul 28, 2011, at 7:42 PM, Jake Penton wrote:

...

I guess I interpret "f::a" to mean "f is some (any) type a". So why can't it be whatever "1" is, which I suppose is Integer. What is the type system looking for? And why does the constraint (Num a) make things ok?

This right here is the core of your confusion. As you probably know, in all major typed "object-oriented" languages this is true; for example, in Java "Object foo;" means that "foo" is some type extending Object, and "List bar;" means that "bar" is some type satisfying the List interface. But in typed functional languages, the mode of "quantification" has the opposite default. In Haskell, 'f::a' means "FOR EVERY type a, f can be that type".

This is universal quantification - just like the upside-down A ("for all") in logic, the type declaration must be true for all values of "a". Sometimes it's important to be clear about which type of quantification you're talking about. When you do, "f :: a" would be written "f :: forall a. a", and what you had in mind would be written "f :: exists a. a". The key difference is that in the "forall" case, the person using 'f' gets to choose its concrete type, but in the "exists" case the concrete type is chosen by the person defining it.

When type classes are involved, they just add restrictions to the type. For example, "f :: Num a => a" still has an implied "forall", but the "Num a =>" part means that instead of "for every type a ...", you have "for every type a which implements Num ...". Similarly, "f :: exists a. Num a => a" would mean "for some type a which implements Num ...". So "f :: a; f = 1" doesn't work because it doesn't restrict the type enough. By restricting the type to "Num a => a", gain the ability to use the functions in the Num class, one of which is "fromInteger", which is called implicitly whenever you use a literal integer - that's what makes integer literals polymorphic in Haskell. Similarly, "f = 3.14" would require "f :: Fractional a => a" because "3.14" implicitly calls "fromRational", a function defined in the Fractional type class.

-- James

PS. Although some Haskell compilers support them as optional language extensions, "forall" and "exists" are not official Haskell syntax - just conventions that humans use to keep things straight when thinking about the types.

Well, there have been a couple of answers on this thread that suggest that a constraint/context will work. But this does not clear things up entirely for me. I probably do not understand your answer. But adding a constraint by itself does not of itself change things, although perhaps you are not suggesting that it would. For example, this does not compile: f :: Fractional a => a f = 3.14 This does: class Foo a where f :: Fractional a => a instance Foo Float where f = 3.14 So I infer that the reason that my example int the original post compiles is something other than merely the presence of the constraint. This compiles: f :: Num a => a f = 1

On 2011-07-29, at 10:02 AM, Daniel Seidel wrote:

On Fri, 2011-07-29 at 09:49 -0400, Jake Penton wrote:

...

For example, this does not compile:

f :: Fractional a => a f = 3.14

I can load this to ghci and also compile

Yeah, sorry - so can I. I must have screwed up earlier. Fat fingers, bleary eyes.... But, getting back to my point (or possibly making an unrelated one for all I know), how about this, which I *hope* I am right in saying does NOT compile, even though Bool is an instance of Ord: g :: Ord a => a g = True It still seems to me that the mere presence of a constraint does not make a difference by itself. Does the difference here lie in compiler calls to fromFractional or fromIntegral in appropriate cases? - J -

On 2011-07-29, at 11:22 AM, Brandon Allbery wrote:

Ask yourself this: is True *every* instance of Ord? You are expecting it to be an "any", but it's an "every" (forall).

By the way, True happens to be an instance of Ord but it doesn't have to be. You're working backwards here, I think. It happens that useful operations on things in class Ord generally produce Bool; that doesn't mean Bool must be Ord.

Right - actually, I did not expect it to compile. I gave the code as, perhaps, a counterexample to what some other responses seemed to be asserting, although it is possible I did not get their point(s) correctly. They seemed to say that adding a constraint is of itself what makes the cases that used numeric literals work. But it seems (as described in Brent Yorgey's post) that there is more to it than that. - J -

On Friday 29 July 2011, 18:14:30, Jake Penton wrote:

On 2011-07-29, at 11:22 AM, Brandon Allbery wrote:

...

Ask yourself this: is True *every* instance of Ord? You are expecting it to be an "any", but it's an "every" (forall).

By the way, True happens to be an instance of Ord but it doesn't have to be. You're working backwards here, I think. It happens that useful operations on things in class Ord generally produce Bool; that doesn't mean Bool must be Ord.

Right - actually, I did not expect it to compile. I gave the code as, perhaps, a counterexample to what some other responses seemed to be asserting, although it is possible I did not get their point(s) correctly. They seemed to say that adding a constraint is of itself what makes the cases that used numeric literals work.

Given the fact that per the report a numeric literal is interpreted as a call to fromInteger or fromRational (depending on whether it's an integer literal or a fractional literal), the addition of the constraint is all that is needed to make it work, since by those functions' types, the value represented by a numeric literal is polymorphic. f = 1 is really f = fromInteger 1& (where n& stands for the Integer of the appropriate value, it's not Haskell; in GHC [with integer-gmp], it would be f = fromInteger (S# 1#) where S# is a constructor of Integer [MagicHash extension required to use it] and 1# is a literal of type Int#, raw signed machine int, four or eight bytes of raw memory). True, on the other hand, is a monomorphic value of type Bool, it cannot have any other type than Bool and trying to specify any other type for it leads to a compile time error.

But it seems (as described in Brent Yorgey's post) that there is more to it than that.

The fundamental difference is monomorphic vs. polymorphic expressions. A monomorphic expression like [True] has a specific type, it doesn't make sense to add constraints to it (but it makes sense to ask whether constraints are satisfied for using it). A polymorphic expression like (toEnum 0) can have many types, but in general the types it can have are constrained by the types of subexpressions/used functions. There is a minimal set of constraints you need to specify, e.g. l = [toEnum 0, 3] needs the constraints (Enum a) and (Num a) in the type signature l :: (Num a, Enum a) => [a] but you can use more or more restrictive constraints to specify a less general type than it could have, for example l :: (Enum a, Bounded a, Num a, Read a) => [a] or l :: (Enum a, RealFrac a) => [a] are valid signatures since they are less general/more constrained than the first one. You could also give a monomorphic signature, l :: [Double], which will compile if and only if the specified type of list elements belongs to Num and Enum.

On Jul 29, 2011, at 9:49 AM, Jake Penton wrote:

Well, there have been a couple of answers on this thread that suggest that a constraint/context will work. But this does not clear things up entirely for me. I probably do not understand your answer. But adding a constraint by itself does not of itself change things, although perhaps you are not suggesting that it would.

For example, this does not compile:

f :: Fractional a => a f = 3.14

It should. Is there something else in the file you're compiling which somehow conflicts? What error does it print?

This does:

class Foo a where f :: Fractional a => a

instance Foo Float where f = 3.14

So I infer that the reason that my example int the original post compiles is something other than merely the presence of the constraint. This compiles:

f :: Num a => a f = 1

Actually, it is solely the presence of the constraint which makes it OK. By constraining it, you're saying "f can produce a value of any type, so long as that type implements Num" - and by saying that, you get to rely on the compiler enforcing it, so you can use all the functions Num provides. One of those functions is "fromInteger", which the compiler uses in the implementation of "1". When you say "f = 1", the compiler interprets that as "f = fromInteger (1 :: Integer)". Without the constraint, you're not allowed to use "fromInteger" because that function doesn't exist for all types. -- James