Reputation: 31
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
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:
(Void, Void) ≅ Void
.Either
gives use two constructors, both require a Void
argument which we can't provide, so we still have Either Void Void ≅ Void
.(Void, ())
because we can't provide a value for the fst
.Left
, but we can do Right ()
! So Either Void () ≅ ()
, because that is the single value of this type.()
.Left ()
and Right ()
.Upvotes: 13