Haskell type functions?

Question

Consider this ADT:

data Property f a = Property String (f a) | Zilch
  deriving Show

What is f here? Is it a function acting on a? Is it a 'type function'? The instructor said that Haskell has a Turing complete type language...so in which case the types can have functions too I assume?

*Main> var = Property "Colors" [1,2,3,4]
*Main> :t var
var :: Num a => Property [] a

How is f behaving like [] here? Since [] is the constructor for the empty list, is f always going to be the outermost empty constructor for the type of a as in the following examples?

*Main> var = Property "Colors" [(1,"Red"),(2,"Blue")]
*Main> :t var
var :: Num t => Property [] (t, [Char])

*Main> var = Property "Colors" (1,"Red")
*Main> :t var
var :: Num t => Property ((,) t) [Char]

The latter one I don't quite get but if someone said Haskell inferred the empty constructor for that tuple, I'm okay buying that. On the other hand,

*Main> var = Property "Colors" 20
*Main> :t var
var :: Num (f a) => Property f a

what is f here? Can't be the identity because id :: a -> a but we need (f a).

I managed to make my ADT a functor with:

instance Functor f => Functor (Property f) where
  fmap fun (Property name a) = Property name (fmap fun a)
  fmap g Zilch               = Zilch 

So something like the following works

*Main> var = Property "Colors" [1,2,3,4]
*Main> fmap (+1) var
Property "Colors" [2,3,4,5]

But what if I gave it to the previous example of a tuple?

I am really looking for explanatory answers (have seen Haskell for barely two months in a summer course), not references to things like FlexibleContexts to allow ... say fmap to work on arbitrary a.

Answer 1

You should read about functors and kinds:

The f there is like a functor, (but it's not a functor) meaning in first place that the type of the type f (the type of a type is named kind in haskell), is * -> *, meaning it takes a type, and returns a type to you.

That's why var = Property "Colors" [1,2,3,4], var has that "rare" type not because [] is the empty constructor of list, is because [] :k is * -> *

Let's see this another example:

var2 = Property "Perhaps A Bool" (Just True)

type of var2 :t :

var2 :: Property Maybe Bool

Why is that, because Maybe also has kind ->, it is waiting for a type to return another, see the type, it doesn't say (Maybe Bool) Bool it says Maybe Bool. Just as your another example, like [] instead [Int]

More about functors and kinds

Answer 2

You've gotten confused by the (confusing) fact that [] means two different things in different contexts in Haskell, which has made it hard for you to interpret the rest of your experiments.

At the value level [] indeed is the empty constructor for lists. But when you asked for the type of Property "Colors" [1,2,3,4] and saw Property [] a you're looking at a type expression, not a value expression. There is no empty list at the type level.¹ Instead [] is the type constructor for the list type. You can have [Int] (the type of lists of ints), [Bool] (the type of lists of bools), or [a] (the polymorphic type of lists of a); [] is the thing that's being applied to Int, Bool, and a in those examples.

You can actually write [Int] as [] Int if you want, though it looks weird, so you usually only see [] at the type level when you want to use it unapplied.

Lets take a look at your data declaration again:

data Property f a = Property String (f a) | Zilch

On the left-hand side you've declared the shape of the type Property; Property f a forms a type. On the right hand side you declare the shape of the values that go in that type, by listing the possible value constructors (Property and Zilch) and the types of the "slots" in those constructors (none for Zilch; one slot of type String and another one of type f a, for Property).

So from that we can tell that whatever f and a are, the type expression f a (f applied to a) must form a type that has values. But f doesn't have to be (in fact it can't be) a normal type of values on its own! There is no slot of type f in the Property value constructor.

A much clearer example to use would have been this:

*Main> var = Property "Stuff" (Just True)
*Main> :t var
var :: Property Maybe Bool

If you don't know it, Maybe is a built in type whose declaration looks like this:

data Maybe a = Just a | Nothing

It's good for this example because we're not using the same name at the type level and the value level, which avoids confusion when you're trying to learn how things work.

Just True is a value of type Maybe Bool. At the value level we have the Just data constructor applied to the value True. At the type level we have the Maybe type constructor applied to the type Bool. Maybe Bool values go in the f a slot of the Property value constructor, which fits straightforwardly: f is Maybe and a is Bool.

So going back to your original example:

*Main> var = Property "Colors" [1,2,3,4]
*Main> :t var
var :: Num a => Property [] a

You're filling the f a slot with [1, 2, 3, 4]. That's a list of some kind of number, so it'll be Num t => [t]. So the a in f a is the t (with a Num constraint that needs to come along), and the f is the list type constructor []. This [] is like Maybe, not like Nothing.

*Main> var = Property "Colors" (1,"Red")
*Main> :t var
var :: Num t => Property ((,) t) [Char]

Here the f a slot is being filled with (1, "Red"), which is of type Num t => (t, [Char]) (remembering that String is just another way of writing [Char]). Now to understand this we have to get a little finicky. Forget the constraint for now, and just focus on (t, [Char]). Somehow we need to interpret that as something applied to something else, so we can match it to f a. Well it turns out that although we have special syntax for tuple types (like (a, b)), they're really just like ordinary ADTs you could declare without the special syntax. A 2-tuple type is a type constructor that we can write (,) applied to two other types, in this case t and [Char]. And we can use partially applied type constructors, so we can think of (,) applied to t as one unit, and that unit applied to [Char]. We can write that interpretation as a Haskell type expression ((,) t) [Char], but I'm not sure if that's clearer. But what it comes down to is that we can match this to f a by taking the first "unit" (,) t as f and [Char] as a. Which then gives us Property ((,) t) [Char] (only we have to also put back the Num t constraint we forgot about earlier).

And finally this one:

*Main> var = Property "Colors" 20
*Main> :t var
var :: Num (f a) => Property f a

Here we're filling the f a slot with 20, some sort of number. We haven't specified exactly what type the number is, so Haskell is willing to believe it could be any type in the Num class. But we still need the type to have a "shape" we can match with f a: some type constructor applied to some other type. And it's the whole type expression f a that needs to match the type of 20, so that's what has a Num constraint. But we haven't said anything else about what f or a might be, and 20 can by any type that meets a Num constraint, so it can be any Num (f a) => f a we want for it, hence why the type of your var is still polymorphic in f and a (just with the added constraint).

You might have only seen numeric types like Integer, Int, Double, etc, and so be wondering how there could possibly be an f a that's a number; all of those examples are just single basic types, not something applied to something. But you can write your own Num instances, so Haskell never assumes a given type (or shape of type) couldn't be a number, it'll just complain if you actually attempt to use it and it can't find a Num instance. So sometimes you get things like this that are probably errors, but Haskell accepts (for now) with a Num type on an odd thing that you weren't expecting.

And in fact there are already types in the built-in libraries that do have compound type-level structore and have a Num instance. One example is the Ratio type for representing fractional numbers as ratios of two integers. You can have a Ratio Int or a Ratio Integer, for example:

Main*> 4 :: Ratio Int
4 % 1

So you could say:

*Main> var = Property "Colors" (20 :: Ratio Integer)
*Main> :t var
var :: Property Ratio Integer

---

¹ Actually there can be, with the DataKinds extension enabled to allow types that mirror the structure of almost any value, so you can have type-level lists. But that's not what's going on here and it's not really a feature you can use until you've got a good handle on the way types and values work in vanilla Haskell, so I recommend you ignore this footnote and pretend it doesn't exist yet.

Answer 3

The instructor said that Haskell has a Turing complete type language...

First of all that claim is wrong. Haskell has no Turing complete type system. There are extensions in GHC to make it Turing complete, but pure Haskell has not Turing complete type system.

How is f behaving like [] here? Since [] is the constructor for the empty list, is f always going to be the outermost empty constructor for the type of a as in the following examples?

You are mixing type constructors with value constructors. Haskell has defined a list as:

data [] a = [] | a : ([] a)

The boldface is the [] type constructor the non-boldface is the value constructor. If you write [] in a type signature you refer to the type. For instance map has type map :: (a -> b) -> [] a -> [] b.

Now as we have seen in the definition of data [], we have a type parameter. We need to apply the [] type to another type before it is a "concrete" type. Therefore the "meta-type" of [] is * -> *: it takes.

The same holds for the type Property, it has meta-type * -> * -> * since it requires two type parameters. Property [] on the other hand has meta-type * -> *.

Answer 4

What is f here? Is it a function acting on a? Is it a 'type function'?

Yes, it is indeed a type function, in the sense that it accepts a type and yields a type, i.e. its kind is Type -> Type – or, as Haskell traditionally writes it

> :k []
[] :: * -> *

How is f behaving like [] here? Since [] is the constructor for the empty list...

That's a misunderstanding. Actually there are two different things called [] in Haskell:

2. The list value constructor [] :: [a]. This generates an empty list (or arbitrary contained-type – since it actually contains zero elements anyway you don't care about that type).

and

1. The list type constructor [] :: * -> *. This takes a type and gives the type of a list containing values of that type. The argument is important, because most interesting lists are obviously not empty.

In Property [] a, you're dealing with the type constructor, which again, unlike the value constructor, is a function which operates on types, therefore you can instantiate it for f.

Property ((,) t) [Char]

Here you've discovered another type-level function: the tuple type constructor. This takes two type arguments and gives a type (that of tuples of these types). With (,) t you already apply it to one type argument, but leave the other open, so again you can use this as a one-argument type function like f.