CODEWITHSUNDEEP
haskellalgebraic-data-typestype-theoryunit-type
user3002392
user3002392

Reputation: 31

Something is really wrong with either ADT theory or how it is treated in programming languages?

I am not a mathematician, but i feel some logical problems are there.

Lets start from the ADT primitives, for example "unit" type. It should play role of "1" in the context of type set. But in fact, we see "unit" type often called equivalent of "void" in C, C++, etc. At the same time we've our own "void" type in ADT, which plays role of "0", and really defines NO values of itself.

Some opinions on that sounds like "unit type brings no information, therefore it is useless and we can think of it as of void-like". But where is C void equivalent? Or, void = unit, "0=1"? It is bad idea bringing some paradoxes.

Then, lets go deeper. Unit type defines only one value, okay. But, why in ADT theory 

unit + unit = 2*unit

when we should get unit? "+" works like "or" defining type that we know as variant types. "unit or unit" definitely doesn't give us "bits", or anything more complex to continue.

Mention haskell tuples, which doesn't have even tuple of single element but can be empty. So it's from ADT theory too. Tuple is a multiplication of item types, therefore one element tuple is the same as that naked element, and empty tuple is unit value (). 

a == (a) == ((a)) == ...
() == (()) == ...

So, a paradox here is: what length does have an empty tuple? As you can see, its length is zero and one at the same time...

Upvotes: 3

Views: 531

Answers (1)

leftaroundabout
leftaroundabout

Reputation: 120751

First, we need to disregard C-like languages etc.: those don't even try to match the mathematical foundations.

Haskell and other functional languages do try this, and while it's often not obvious how the isomorphisms work they are there.

Then, lets go deeper. Unit type defines only one value, okay. But, why in ADT theory

unit + unit = 2*unit

when we should get unit? "+" works like "or" defining type that we know as variant types. "unit or unit" definitely doesn't give us "bits", or anything more complex to continue.

Well, yes, it does give us bits.

type Bit = Either () ()

(||), (&&) :: Bit -> Bit -> Bit

(Left()) || (Left()) = Left()
_ || _ = Right()

(Right()) && (Right()) = Right()
_ && _ = Left()

If you don't believe it works:

Prelude Acme.Missiles> type Bit = Either () ()
Prelude Acme.Missiles> let [true, false] = [Left (), Right ()] :: [Bit]
Prelude Acme.Missiles> if true==false then launchMissiles else return ()
Loading package stm-2.4.2 ... linking ... done.
Loading package acme-missiles-0.3 ... linking ... done.
Prelude Acme.Missiles>

Ah, thank goodness, we're still alive...

As for "nested unit tuples": those just represent the fact that 1ⁿ ≡ 1.

Perhaps things become clearer when we actually consider the zero type as well.

{-# LANGUAGE EmptyDataDecls #-}

data Void

now, let's go through the simplest cases:

  • 0*0 = 0. Since we can not offer a value for either side of the tuple, we can't define a value of type (Void, Void) ≅ Void.
  • 0+0 = 0. While Either gives use two constructors, both require a Void argument which we can't provide, so we still have Either Void Void ≅ Void.
  • 0*1 = 0. We can't construct a (Void, ()) because we can't provide a value for the fst.
  • 0+1 = 1. Aha! We can't construct the Left, but we can do Right ()! So Either Void () ≅ (), because that is the single value of this type.
  • 1*1 = 1. Both sides of the tuple can only take on the value ().
  • 1+1 = 2. That's the case I dicussed above, it has the distinct values Left () and Right ().
  • 2+3 = ... darn, I've chosen the wrong programming language for explaining this! BTW, ⟂ is right out...

Upvotes: 13

Related Questions