How many kinds of bottom are there in GHC?

Learn
#1

In another thread bottoms ⊥ and levity are discussed. The classic interpretation of bottom is “does not yield a value when evaluated”, e.g. in every lifted type there is

bottom :: a
bottom = bottom

where evaluating bottom causes an infinite loop. Now the GHC commentary on the type Type says that A type is lifted iff it has bottom as an element. In particular, Int# is unlifted and thus should not have a bottom element. Nevertheless, one can define the function

unpack :: Int -> Int#
unpack (I# x) = x

But where does unpack map bottom to? Certainly no number. The documentation says that there is no ⊥ in Int#. But apparently there is: One can evaluate unpack bottom and GHCi will throw a type error at run-time. So it seems there are three kinds of bottoms:

  1. bindable divergent bottoms of lifted types, as in bottom = bottom
  2. unbindable bottoms of unlifted types, as in unpack bottom. Unbindable in the sense that bot = unpack bottom does not compile, yet as an expression it clearly exists.
  3. bindable errors as in Prelude.undefined that when evaluated cause the RTS to abort immediately.

The wiki page for ⊥ glosses over the second kind.
My question is: Could there exist an implementation of Haskell where unpack does not compile? That is, is the existence of unpack a deficiency in GHCs implementation of unlifted types or a necessary wart in any implementation of lambda calculus with pattern matching?

I have the impression that if we define “A type X has x as an element” as “One can write a named top-level expression of type X that evaluates to x” then indeed Int# has no bottom, but if we accept the more permissive definition "A type X has x as an element if there exists a function f with f () = x" then we must conclude that Int# has a bottom.

4 Likes
Levity should be on the arrow, not on the kind
#2

The following ticket is probably strongly related: #17521: Consider top-level unlifted bindings · Issues · Glasgow Haskell Compiler / GHC · GitLab
We currently cannot have toplevel bindings for unlifted things like Int#.

#3

It does? Hmm:

# ghci -XMagicHash
GHCi, version 9.4.7: https://www.haskell.org/ghc/  :? for help
ghci> :m GHC.Exts
ghci> bottom = bottom
ghci> unpack (I# x) = x
ghci> unpack bottom

<interactive>:4:1: error:
    • Couldn't match a lifted type with an unlifted type
      When matching types
        a0 :: *
        Int# :: TYPE 'IntRep
    • In the first argument of ‘print’, namely ‘it’
      In a stmt of an interactive GHCi command: print it
ghci>

…no - print is an overloaded definition, so it only works for lifted types. Solution - wrap unpack bottom with I#:

ghci> I# (unpack bottom)

^CInterrupted.
ghci>

So unpack bottom actually has the same behaviour as bottom, because unpack is (necessarily) strict.

#4

Similarly

ghci> I# (unpack undefined)
*** Exception: Prelude.undefined
...

has the same behaviour as undefined.

#5

Thanks @DavidB the linked thread contains a trick posted by @jaror to obtain a top-level binding for unlifted bottom:

{-# LANGUAGE ConstraintKinds, StandaloneKindSignatures, PolyKinds, RankNTypes #-}

import GHC.Types
import GHC.Exts

type Lev :: TYPE r -> Type
type Lev a = (() :: Constraint) => a

u :: Lev Int#
u = unpack bottom

So now we do have a named bottom in Lev Int# which GHC says is of kind * so not technically unlifted, but morally so.

That is to be expected: the function I# maps Int# to Int and obviously can not return a number for the argument unpack bottom. This is my point: There is an element in Int# that is not a number, as you have provided a function call f x in which x :: Int# but this x does not behave as any number.

#6

The call to bottom (as argument to unpack) hasn’t produced any element. So we can’t say there was something in Int#.

#7

That implies that Haskell functions are not functions in the mathematical sense. That is what the concept of bottom was invented for in the first place: To be able to give semantics to functional languages where a function call may not produce an element. If you did away with the requirement that a (pure) Haskell function is a mathematical function, then you would not need bottoms at all.

1 Like
#8

Continuing that ghci session:

ghci> div# x y = case x of 0# -> 0#; _ -> 1# +# div# (x -# y) y 
ghci> I# (div# 4# 2#)
2
ghci> I# (div# 4# 0#)
*** Exception: stack overflow
ghci>

I’m now thinking categories 2 and 3:

could be two specific cases of something more generic…

#9

Well yeah, I’d say that any Haskell function from a lifted domain to an unlifted codomain is not a mathematical function. The lifted types and their functions form a category-like thing, and the unlifted types and their functions form another category-like thing, and since there’s an inclusion from the unlifted types to the lifted types we can take an arrow in the unlifted category-like thing and compose it with the inclusion to get a mathematical function from unlifted domains to lifted codomains, but not the other way around.

#10

What about constant functions that map ⊥ to a total value? They can be given semantics as a mathematical function.
Lifted types and functions live in the category CPO, the category of directed complete partial orders with ⊥ and continuous maps as arrows. Unlifted types live in the category DCPO of directed complete partial orders, of which CPO is a full sub-category. Thus both lifted and unlifted types can co-exist in the same category. DCPO is also cartesian closed.

#11

Indeed not a true category, since thanks to RankNTypes there are definable functions f and g such that f.g does not type-check.

#12

Yes, indeed they have in common that they observably do not yield a value, as they instantly trigger a certain behaviour in the RTS, while bottom being semantically ⊥ can not be observed.

#13

Ah, you got me there! I should weaken my statement to ‘… is not necessarily a mathematical function’.

My main point is that unpack is a cheat because you can’t interpret its definition as purely in the lifted category-like thing or the unlifted category-like thing (because either would require composing, before or after, with the inverse of the inclusion, in order to get the advertised type). It’s something other than a native arrow of one of those models, and whatever it does should be filed under ‘software’ instead of ‘math’.

#14

…but with some difficulty, if I’m correctly interpreting section 6d (pages 147-148 of 169) of Law and Order in Algorithmics (1992).

(…I’m now wondering if Ganule’s relative monad concept mentioned in this presentation (at 24:10) could be of some use here.)

#15

So regardless of whether bottoms of kind 2 and 3 are instances of a common thing, can we agree on either of:

(a) The statement A type is lifted iff it has bottom as an element either requires a very careful definition of has … as an element or is plainly false.

(b) Either we acknowledge that Haskell with unlifted types can not be given denotational semantics in a category of structured sets and functions or that some typing judgements of GHC are wrong.

(c) If we insist that the pure fragment of Haskell as accepted by GHC can be given denotational semantics as sets and functions AND we insist that unlifted types have no bottom, then programs like unpack should not compile.

#16

Regarding (c): if unpack was “banned”, I suspect that would have dire ramifications for certain GHC transformations (right now, I’m thinking of the worker-wrapper one; there are probably others).

Regarding (b): either option seems plausible given recent threads here.

Regarding (a): could (b) be considered a consequence of it i.e:

  • by not having that careful definition (if one exists at all!),
  • or being false,

due to the presence of unlifted types in (Glasgow) Haskell…?

#17

It’s (slightly) wrong to say "there is no ⊥ in Int#" without further qualification.
There is a difference between a computation returning Int# or an argument/let binder binding an Int#.

A computation such as unpack bottom returning an unlifted value may well diverge in a Turing-complete language, even in a strict one!
However, a function blah x = x +# 42# will never diverge when it inspects an unlifted argument.
Whenever you have x :: Int#, you can be sure that you don’t need to evaluate it, or rather that evaluating it (i.e., calling its code) would return immediately. It’s a bit confusing to use Int# as the example here as it is also unboxed and hence is not really represented by a pointer to code like Int.

Unliftedness is a precondition on the domain of a function, because it says “never call me with ⊥ because I don’t know what to do!” It’s the same as blub x = x + y expecting an Int as parameter, and you must never call it with False.

So to answer your questions:

But where does unpack map bottom to?

to bottom. It is an arbitrary computation, so it may do that.

unbindable bottoms of unlifted types, as in unpack bottom. Unbindable in the sense that bot = unpack bottom does not compile, yet as an expression it clearly exists.

This is a restriction for top-level bindings, #17521, linked to by @DavidB.

bindable errors as in Prelude.undefined

This is in fact pretty tricky; Prelude.undefined has type HasCallStack => a, so it has lifted type due to the constraint. If it hadn’t we wouldn’t be able to write blah x = x +# (undefined :: Int#). What happens here is actually a function call with the HasCallStack dictionary; a computation that ultimately produces an Int#. Try let x = undefined :: Int# in I# (42# quotInt# (0# +# x)); you will find that it has to evaluate the RHS of x before the div by zero in order to uphold that x :: Int# may not evaluate to bottom.

I don’t see any deficiencies here. This all follows by the denotational semantics of strict languages.
In a strict language, eval :: Exp -> (Var -> Value) -> Either Value ⊥, and the ⊥ you are seeing is that of the result, not one somewhere in Value.

1 Like
#18

My favourite interpretation would be:
As @AntC2 observed, from the viewpoint of denotational semantics all three proposed kinds of bottom are identical, since denotational semantics only knows one bottom and disregards the operational stuff happening in the RTS.
(a): The statement is false due to underspecified wording: Every type has ⊥ but some are bindable and some are not, which is, given the discussion @DavidB linked to, just a current choice of the GHC devs and not a type-theoretical limitation. @sgraf above provides the context in which that statement is to be interpreted. All types being objects of CPO makes the type theory much nicer, and that category still does allow notions of strictness, unboxed tuples and so forth. Furthermore, Int can still be distinct from Int# as ⊥ is observably distinct from I# (⊥ :: Int#).
(b): The typing judgemement of unpack is correct and no contradiction arises if we acknowledge the existence of ⊥ in unlifted types as available targets of functions.
(c): The statement is correct because one of the antecedents of the implication is false.

This touches the second interpretation of the specialisation order: Since unlifted, unboxed types are “flat” except for the ⊥ underneath everything else, there is no place for thunks in the semantic domain. So I would relativize the statement to: “If you have a value of Int#, you can be sure that you don’t need to evaluate it, since that won’t change anything: x is either ⊥ so evaluation does not return, or it was already evaluated.”

But note that Either (even the strict version) places the ⊥ next to Value whereas a diverging computation in the domain model is underneath everything else. So instead of Either one should use a type constructor like Lift :: ? -> *. If it was really an Either, then one could pattern match on it and solve the halting problem.

That does not type-check, given that bottom :: forall (a :: *). a. It is a different ⊥ not representable by bottom and not by something like undefined, as that also requires a lifted type.

#19

So I would relativize the statement to: “If you have a value of Int#, you can be sure that you don’t need to evaluate it, since that won’t change anything: x is either ⊥ so evaluation does not return, or it was already evaluated.”

No, this is precisely not the case. x::Int# can’t bind ⊥, period. That is because Int# is contained in the by-value domain Value I hinted at above, and Value does not contain ⊥.

However, eval may either terminate with a Value or diverge returning ⊥. The use of Either was to be interpreted as set union; let us not mix up bottoms introduced by the laziness of the presumed meta language Haskell with semantic ⊥ in the semantic domain of the object language Exp. I did not say anything about the order relationship in Value + ⊥; of course there is one and it isn’t pretty nor interesting for what we discuss here.

That does not type-check, given that bottom :: forall (a :: *). a

Perhaps I should have taken more care and not mix up semantic ⊥ with Haskell’s definition of undefined/your bottom. Both bottom and unpack bottom have the same denotation ⊥. The former is syntax, the latter is semantics.

#20

Agreed, but pardon my hair-splitting: You said Whenever you have x without saying what exactly have means and whether x is necessarily an identifier or a meta-syntactic construct. If have means bound to an identifier then what you state may well be correct. If have means “occurs as a sub-expression somewhere in the program”, then unpack bottom proves that x can be ⊥, as @jaror demonstrated.