Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Is a Haskell type constructor 'just' a function?

I am going through "Haskell Programming from first principles" and found an exercise asking if the following [code slightly edited here] was valid:

module Test where

type Subject = String
type Verb = String
type Object = String

data Sentence = 
  Sentence Subject Verb Object
  deriving (Eq, Show)

a1 = Sentence "I" "like" "cheese"
a2 = Sentence "I" "scream"

My expectation was initially that the code would fail, because in the definition of a2, Sentence only had two arguments. But found that GHCi was happy to load the module. I did a little experimentation and found that I could now type

a3 = a2 "icecream"

and a3 (typed into GHCi) would print Sentence "I" "scream" "icecream". Also, if I inquire the types of a2 I get a2 :: Object -> Sentence. So if I understand correctly, a2 is behaving exactly like a partially-applied function.

Question therefore is: Is a type constructor really just a function (that returns a type value) in all situations - distinguished from a 'normal' function only in that it has to start with an upper-case character?

like image 755
Penguino Avatar asked May 26 '21 09:05

Penguino


People also ask

What is type constructor in Haskell?

Type constructor Of any specific type a , be it Integer , Maybe String , or even Tree b , in which case it will be a tree of tree of b . The data type is polymorphic (and a is a type variable that is to be substituted by a specific type). So when used, the values will have types like Tree Int or Tree (Tree Boolean) .

What is constructor data type?

A data constructor is a "function" that takes 0 or more values and gives you back a new value. A type constructor is a "function" that takes 0 or more types and gives you back a new type.

Is functor a type constructor?

We use the word “functor” to refer to type constructors that meet certain criteria. Most often, what we mean is a type constructor that has a sensible instance of the Functor class.

Which constructor is called a type constructor?

In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old ones. Basic types are considered to be built using nullary type constructors.


1 Answers

First off, what you're talking about here are data constructors, not type constructors. The example happens to contain both a (nullary) type constructor Sentence and a ternary data constructor Sentence. To make it clear which is which:

data SentenceTC = SentenceDC Subject Verb Object

SentenceTC is a type constructor, SentenceDC is a data constructor.

So, the question is:

Is SentenceDC just a function?

and the answer is, it is a function, but not “just” a function. It is specifically an injective function, i.e. every combination of arguments leads to a different result. Because of that, it is always possible to infer which arguments it was, from the resulting SentenceTC value. And that's what happens when you pattern match on a constructor.

a1Verb :: Verb
a1Verb = case a1 of
    Sentence _ v _ -> v

This would not be possible with a general function, like

n' :: Int
n' = abs n
 where n = -3

nNew :: Int
nNew = case n' of
   abs n -> n   -- error, `abs` can not be used as a pattern match

And that wouldn't make sense either, because there are actually two different numbers whose abs is equal to n' (namely, -3 and 3).

But yeah, SentenceDC is a function, you can do everything with it that you could do with other functions of type String -> String -> String -> SentenceTC. Not the other way around though: not everything you can do with a data constructor can also be done with a general function of the same type.

like image 66
leftaroundabout Avatar answered Sep 28 '22 08:09

leftaroundabout