Home > Software design >  Understanding double colon "::" and type variables in Haskell?
Understanding double colon "::" and type variables in Haskell?

Time:10-24

For a uni assignment, a function "lookup" has been defined as:

lookup :: Env e -> String -> Maybe e

The "Env" keyword has been defined as:

import qualified Data.Map as M
newtype Env e = Env (M.Map String e) deriving (Functor, Foldable, Traversable, Show, Eq, Monoid, Semigroup)

I understand that the double colon "::" means "has type of". So the lookup function takes two arguments and returns something. I know the second argument is a string, however, I'm struggling to understand the first argument and the output. What is the "Env" type and what does the "e" after it represent. It feels like e is an argument to "Env" but if that is the case, the output wouldn't make sense.

Any help would be appreciated.

CodePudding user response:

It feels like e is an argument to "Env" but if that is the case, the output wouldn't make sense.

That's the direction the syntax is trying to "feel like", because that's what it means. Env is a parameterised type, and e is being passed as an argument to that parameter.

I'm not 100% sure why you think the output wouldn't make sense, under that interpretation? Maybe is also a parameterised type, and the variable e is also being passed to Maybe; this is no different than using a variable twice in any piece of code. You can think of it as something like this pseudo-code:

lookupType(e) {
  argument1_type = Env(e)
  argument2_type = String
  result_type = Maybe(e)
}

Is your confusion that you are thinking of e in the type signature of lookup not as being passed to Env, but as being defined to receive the argument of Env? That happens in the place where Env is defined, not where it is used in the type of lookup. Again, this is just like what happens at the value level with function arguments; e.g. when you're writing code to define a function like plus:

plus x y = x   y

Then the x and y variables are created to stand for whatever plus is applied to elsewhere. But in another piece of code where you're using plus, something like incr x = plus x 1 here the variable is just being passed to plus as an argument, it is not defined as the parameter of plus (it was in fact defined as the parameter of incr).

Perhaps the thing that you need more explicitly called out is this. lookup :: Env e -> String -> Maybe e is saying:

For any type e that you like, lookup takes an Env e and a String and returns a Maybe e

Thus you could pass lookup an Env Integer and a String, and it will give you back a Maybe Integer. Or you could pass it an Env (Maybe [(String, Float)]) and a String, and it will give you back a Maybe (Maybe [(String, Float)]). This should hopefully be intuitive, because it's just looking up keys in an environment; whatever type of data is stored in the environment you pass to lookup is the type that lookup will maybe-return.

The e is there because in fact lookup is parametrically polymorphic; it's almost like lookup takes a type argument called e, which it can then pass to other things in its type signature.1 That's why I wrote my pseudo-code the way I did, above.

But this is just how variables in type signatures work, in base Haskell2. You simply write variables in your type signature without defining them anyway, and they mean your definition can be used with ANY type at the position you write the variable. The only reason the variables have names like e (rather than being some sort of wildcard symbol like ?) is because you often need to say that you can work with any type, but it has to be the same type in several different places. lookup is like that; it can take any type of Env and return any sort of Maybe, but they have to be consistent. Giving the variable the name e merely allows you to link them to say that they're the same variable.


1 This is in fact exactly how types like this work at a lower level. Haskell normally keeps this kind of type argument invisible though; you just write a type signature containing variables, without defining them, and every time you use the accompanying binding the compiler figures out how the variables should be instantiated.


2 In more advanced Haskell, when you turn on a bunch of extensions, you can actually control exactly where type variables are introduced, rather than it always happening automatically at the beginning of every type signature you use with variables. You don't need to know that yet, and I'm not going to talk about it further.

CodePudding user response:

I'll try to give concrete examples, providing and motivating intuition. With thtat intuition, I think the question has a very natural answer:

e is a type variable, and the lookup function wants to work on all possible environments, regardless of which concrete type e is". The unbound e is a natural way to syntactically express that

Step 1, the Env type

The Env type is a wrapper for Map type in the Data.Map module in the containers package. It is a collection of key-value pairs, and you can insert new key-value pairs and look them up. If the key you are looking up is missing, you must return an error, a null value, a default or something else. Just like hashmaps or dictionaries in other programming languages.

The documentation (linked above) writes

data Map = Map k a

A Map from keys k to values a. and we will try that out and wee what k and a can be. I use ghci to get interactive feedback.

Prelude> import Data.Map as M
Prelude M> map1 = M.fromList [("Sweden","SEK"),("Chile","CLP")]
Prelude M> :type map1
map1 :: Map [Char] [Char]
Prelude M> map2 = M.fromList [(1::Integer,"Un"),(2,"deux")]
Prelude M> :type map2
map2 :: Map Integer [Char]
Prelude M> map3 = fromList [("Ludvig",10000::Double),("Mikael",25000)]
Prelude M> :type map3
map3 :: Map [Char] Double

You can see that we create various mappings based on lists of key-value pairs.The type signature in the documentation Map k a correspond to different k and a in the ghci session above. For map2, k correspongs to Integer and a to [Char]. You can also see how I declared manual types at some places, using the double colon syntax.

To reduce the flexibility, we can create a new "wrapping" type that for M.Map. With this wrapper, we make sure that the keys are always Strings.

Prelude M> newtype Env e = Env (M.Map String e) deriving (Show)

this definition says that the type Env e is, for every e an alias for M.Map String e. The newtype declaration further says that we must always be explicit and wrap the mappings in a Env value constructor. Let see if we can do that.

Prelude M> Env map1
Env (fromList [("Chile","CLP"),("Sweden","SEK")])
Prelude M> Env map2

<interactive>:34:6: error:
    • Couldn't match type ‘Integer’ with ‘[Char]’
      Expected type: Map String [Char]
        Actual type: Map Integer [Char]
    • In the first argument of ‘Env’, namely ‘(map2)’
      In the expression: Env (map2)
      In an equation for ‘it’: it = Env (map2)
Prelude M> Env map3
Env (fromList [("Ludvig",10000.0),("Mikael",25000.0)])

In the session above, we see that both map1 and map3 can be wrapped in an Env, since they have an appropriate type (they have k==String), but map2 cannot (having k==Integer).

The logical step from Map to Env is a little tricky, since also renames some variables. What was called a when talking about maps, is called e in the Env case. But variable names are always arbitrary, so that is ok.

Step 2, the lookup

We have established that Env e is a wrapping type that contains a lookup table from strings to values of some type e. How do you lookup things? Let us start with the non-wrapped case, and then the wrapped case. In Data.Map there is a function called lookup. Lets try it!

Prelude M> M.lookup "Ludvig" map3
Just 10000.0
Prelude M> M.lookup "Elias" map3
Nothing

Okay, to look up a value, we supply a key, and get just the corresponding value. If the key is missing, we get nothing. What is the type of the return value?

Prelude M> :type M.lookup "Ludvig" map3
M.lookup "Ludvig" map3 :: Maybe Double

when making a lookup in a Data [Char] Double, we need a key of type [Char] and return a vlue of type Maybe Double. Okay. That sounds reasonable. What about some other example?

Prelude M> :type M.lookup 1 map2
M.lookup 1 map2 :: Maybe [Char]

when making a lookup in a Data Integer [Char], we need a key of type Integer and return a value of type Maybe [Char]. So in general, to lookup we need a key of type k and a map of type M.Map k a and return a Maybe a.

Generally, we think M.lookup :: k -> M.Map k a -> Maybe a. Lets see if ghci agrees.

Prelude M> :t M.lookup
M.lookup :: Ord k => k -> Map k a -> Maybe a

It does! It also requires that the k type must be some type with a defined order on it, such as strings or numbers. That is the meaning of the Ord k => thing in the beginning. Why? Well, it has to do with how M.Map type is defined... do not care too much about it right now.

We can specialize the type signature if we set k to be String. In that special case, it would look like

M.lookup :: String -> Map String a -> Maybe a

hmm. this inspires us to flip the order of argument 1 and 2 to lookup, and replace the variable a with e. It is just a variable, and names on variables are arbitrary anyways... Lets call this new function myLookup

myLookup :: Map String e -> String -> Maybe e

and since Env a is essentially the same as Map String e, if we just unwrap the Env type, we may define

myLookup :: Env a -> String -> Maybe e

how does one implement such a function? One way is to just unwrap the type by pattern matching, and let the library to the heavy lifting.

myLookup (Env map) key = M.lookup key map

Conclusion

I have tried to build up concrete examples using functions and types from the standard library of Haskell. I hope I have illustrated the idea of a polymorhic type (that M.Map k a is a type when supplied with a k and a v) and that Env is a wrapper, specializing to the case when k is a String.

I hope that this concrete example motivates why the type signatures looks like they do and why type variables are useful.

I have not tried to give you the formal treatment with terminology. I have not explained the Maybe type, nor typeclasses and derived typeclasses. I hope you can read up on that elsewhere.

I hope it helps.

  • Related