2

Disclosure: I'm a Scala Programmer learning Haskell.

I'd like to understand type variable behaviour a bit better.

Contrary to Scala it seems we can declare variable of generic type (i.e. type variable). That is generic are not limited to function. However I can't understand the following deprecencies and would like some explanation for this.

Why is it that the following code does work on function:

g :: a -> a -- a can take the concrete type Num a => a or something else like Bool
g x = x

g 10
--g 10 :: Num a => a

g True
--g True :: Bool

However the following strange thing happen with variable as opposed to function

e :: a
e = 1
--  No instance for (Num a) arising from the literal ‘1’
--      Possible fix:
--      add (Num a) to the context of
--        the type signature for:
--          e1 :: forall a. a
--    In the expression: 1
--    In an equation for ‘e1’: e1 = 1

Same thing of course if I type the following in the REPL

e :: a; e = 1

Q1 ) From that it would seem we have a difference of Behaviour of generic type (i.e. type variable) between variable and function ? Why is that ? or what is it i am not seeing or getting yet ?

Now the strange part

If in the Repl however I do

 e :: a; e = undefined

and then

e = 1

then i get

:t e
-- e1 :: Num p => p

So using undefined in the REPL "at least", I get back the Behaviour of Generic type on function.

Q2) What actually is going on here ? This all thing doe not sound super coherent to me. Can anyone explain please ?

MaatDeamon
  • 9,532
  • 9
  • 60
  • 127
  • 2
    `e :: a` means `e` can be of **any** type. Not any type **you** want, but any type *any code that could possibly use `e` could possibly want*. – n. m. could be an AI Jan 04 '21 at 10:57
  • Thanks for the answer. However i do not understand the difference of behavior exposed above. Could you please help me make sense of it ? – MaatDeamon Jan 04 '21 at 10:59
  • 3
    OK, let's see. If you write `g :: a -> a; g x = 42 + x`, you will get an error, not unlike the error you are getting for `e::a`. Does this error make sense to you? – n. m. could be an AI Jan 04 '21 at 11:05
  • Regarding the second `e = 1` in repl, this is a completely new, unrelated definition of `e` that masks the old definition. In repl, you can redefine a name as many times as you want. The old definition is simply forgotten. – n. m. could be an AI Jan 04 '21 at 11:08
  • Same type of error the other way around indeed. Still i can't phrase the explanation. If you would help make sense for someone learning, that would be great :) – MaatDeamon Jan 04 '21 at 11:08
  • alright, understood for the second e – MaatDeamon Jan 04 '21 at 11:09
  • So what is happening with ```g :: a -> a; g x = x``` working and not ```g :: a -> a; g x = 42 + x ``` – MaatDeamon Jan 04 '21 at 11:11
  • I suspect ```g :: a -> a; g x = 42 + x``` would not work for all a right ? – MaatDeamon Jan 04 '21 at 11:12
  • 4
    You can view it this way. `g :: a -> a` has many types. `Int->Int`, `String->String` and `Bool->Bool` are all types of `g`, `a->a` is simply the most generic of these types. The equation `g x = x` does not contradict any of these types. Likewise, `e :: a` has many types (all possible types really), including `Int`, `String`, `Bool` and `Int->Int` (so you can legally write `e == "abc"` or `e 42`). However, the definition `a = 1` doesn't match most of these types. – n. m. could be an AI Jan 04 '21 at 11:12
  • 2
    A small correction, the old definition is not forgotten, but made invisible (it is still available to other definitions that reference the old definition). – n. m. could be an AI Jan 04 '21 at 11:17
  • 1
    Very good clarification Sir !!! Thank you. I would suggest if you have time, that you make an answer of this. So (1) I can up vote, (2) and other in my path, who may not get it at first as me, would benefit to have an official answer. – MaatDeamon Jan 04 '21 at 11:26
  • You might also like [Why can a Num act like a Fractional?](https://stackoverflow.com/questions/42820603), where I give a low-level, mechanical way to reason through what will and will not work, and [Lifting a higher order function in Haskell](https://stackoverflow.com/q/9243215), where I give a discussion of the covariance vs. contravariance issue that explains why `g` and `e` have different instantiation behavior, while pretending that type inference is a kind of subtyping thing (which may be a more comfortable read for you, specifically). – Daniel Wagner Jan 04 '21 at 19:37
  • Many thanks for this. Will look into it and comment back once absorbed :) ! – MaatDeamon Jan 04 '21 at 19:54

1 Answers1

6

Type variables in Haskell are universally quantified. This means that the actual type of g is

g :: ∀ a . a -> a

The quantifier is normally implicit, but you can actually spell it out in Haskell source (as forall) if you enable certain GHC extensions.

What does it mean? Well quite literally, g has type a -> a for all possible values of a. That is, g is a Bool->Boll and a String->String and an Int->Int function. It has all of these types.

When you write g x = x, you are not breaking the promise given by the type of g, namely, that the argument can be of any type and the result must be of the same type. Indeed, the result is x and the argument is also x, and x obviously has the same type as x.

However, if you write g x = x + 42, this breaks the promise. x cannot be of type Bool or String any more. So the compiler will complain.

Now, the notation

e :: a

in a very similar way should be interpreted as

e :: ∀ a . a

This means e has type a for all possible values of a. That is, it has every possible type: Int and String and Bool and Int->Int and infinitely many others.

You could satisfy the type by defining e as

e = undefined

(and indeed this is basically the only way you can satisfy it). However, if you write

e = 1

you break the promise given by the type of e. So you will get the same kind of error as above.

If you write e = undefined and afterwards e = 1, then in a REPL the second definition shadows the first one, so you have two different variables named e, each of its own type. If you are using REPL you can redefine any name at any time you want, this is what REPL is for! This is of course impossible in a normal Haskell module.

n. m. could be an AI
  • 112,515
  • 14
  • 128
  • 243