haskell - Meaning of "=" in type declaration in Hashkell

Question

As I learn Haskell, I can't help but try to understand everything from a formal point of view. After all this is the theoretical coherence I came to look for as a Scala Programmer.

One thing that does compute well in my mind, is fitting the meaning of type declaration in the overraching theory of lambda calculus and everything is an expression. Yes there is Binding, but Binding does not work with type declaration either.

Example

data DataType a = Data a | Datum 

Question:

1. What is the meaning of = here? If it was the declaration of a function, then on the rhs we would get an expression reducible to an irreducible value or another expression (i.e. returning a function). This is not what we have above.

My confusion

We have a type function in DataType a, and Data Constructor a.k.a Value Constructor in Data a and Datum. Clearly a type is not equal to a value, one is at the term level and the other at the type level. Not the same space at all. However it might work to follow the pronunciation provided here https://wiki.haskell.org/Pronunciation. = is pronounced is. As in a DataType is those values. But that is a stretch. because it is not the same semantic as for a function declaration. Hence I'm puzzled. A Type Level function equal a value level function makes no sense to me.

My question reformulated differently so to explain what i am looking for

So in a sense, I would like to understand the semantic of a data declaration and where does it fit in everything is an expression (Haskell theoretical framework) ?

2. Clarifying the difference with Binding. Generally speaking, when talking about binding, can we say it is an expression of type Unit ? Otherwise, what is it, and what is the type of it, and where does it fit in lambda calculus or whatever we should call the theoretical framework that backs Haskell ?

question from:https://stackoverflow.com/questions/65599412/meaning-of-in-type-declaration-in-hashkell

Answer 1

I think the simplest answer here is that = doesn’t have any one meaning in particular — it is simply the syntax which the Haskell designers decided to use for data types. There is no particular relationship between the = used in function definitions and the = used in ADT definitions; both constructions are used to declare something on the LHS using some sort of specification on the RHS, but that’s about it. The two constructions have more differences than similarities.

As it happens, modern Haskell doesn’t necessarily require the use of = when defining an ADT. The GADTSyntax and GADTs GHCI language extensions enable ‘GADT syntax’, which is an alternate method to define ADTs. It looks like this:

data DataType a where
    Data :: a -> DataType a
    Datum :: DataType a

This illustrates that the use of = is not necessarily a mandatory part of type declarations: it is simply one convention amongst many.

(As to why the Haskell designers chose to use the convention with =, I’m not entirely sure. Possibly it might have been by analogy with type synonyms, like type Synonym = Maybe Int, in which = does have similarities to its use in function definitions, in that the RHS expresses a type which is then assigned the name on the LHS.)