Bottom Type in F# | Hacker News Reader

Bottom Type in F#

tysonwilliams.coding.blog

55 pointsadelarsq52 comments

One of the remarkable property of ML languages is algebraic data types and then type systems. Look here

type Bottom = private Bottom of Bottom

Modeling any kind of data is intuitive and simple. This is why ML languages (F#, oCamel etc.) shines in industries where you've complex data like Finance. Reading any F# code is like reading a novel. It starts with modeling of data and small functions. Then these small functions and data evolves into bigger features. File by file you keep moving upwards. For example if you are writing a Json parser in F#, you start with Modeling Json data first. And here it is

Then everything starts from here.

I would say algebraic data type is the number 1 reason Swift is becoming so popular.

The syntax may not be as elegant as ML languages, but it's still by far the best amongst the "mainstream" languages.

> I would say algebraic data type is the number 1 reason Swift is becoming so popular.

Let's not kid ourselves - iOS is the #1 reason Swift has any popularity at all. Outside of the Apple ecosystem Swift is practically non-existent.

However, I would be interested in server-side Swift if anyone has good use cases or resources.

fair enough. By "popular" i should have said "beloved".

Objective-c was hated by pretty much everyone, and was mainly used because of iOS.

i've yet to find an iOS developer that actually doesn't wish he could code in swift on the server side. It's a really pleasant language.

While I love that Python bolted on a type system, I wish it could do this. I need recursive types about twice a month, and Python just isn't doing it for me. (And while I'm complaining, the replace function for dataclasses is totally kneecapped by not being able to type check its field assignments.)

Bottom types get difficult in presence of statically dispatched type classes / traits. Even though the bottom type doesn't have values, because it is an existing type you can still define traits on it. You could plausibly define any existing trait on it, or none at all, because it's logically consistent the either way: because the values don't exist, you can't actually call the trait methods so any trivial implementation (such as method that panics / throws and exception when called) will do. You won't get logical contradiction because you can't call it.

But then you get the difficulty of, which actual traits should that type implement? That's a hard decision to make, and it's the reason why Rust doesn't yet have a first class bottom type.

> But then you get the difficulty of, which actual traits should that type implement? That's a hard decision to make

No it's not? It implements every trait. That's the whole point of it being a bottom type.

Then you might get logical inconsistencies with traits that are designed to be mutually exclusive and are used in type-level programming.

There's a whole 6.1 section in "Java and Scala Type Systems are Unsound" [0] dedicated to "nonsense types".

[0] https://raw.githubusercontent.com/namin/unsound/master/doc/u...

It gets problematic with associated types/constants/functions. For instance, given the following Rust trait:

  trait Foo {
    type AssocType;
    const ASSOC_CONST: i32;
    fn assoc_fn() -> i32;
  }

what would the following evaluate to if `!` automatically implemented `Foo`?

  <! as Foo>::AssocType
  <! as Foo>::ASSOC_CONST
  <! as Foo>::assoc_fn()

These can all occur in reachable code because they do not depend on `!` having inhabitants.

Compiler error if these are ever instantiated/need to be monomorphised? The problem is that this is very unrustic by having the error be very non local.

But maybe this is unavoidable once you have sufficiently complex const fn anyway...

There's a principle in Rust that only the function signature is needed to know if a function call is valid, without any need to look at the function body.

It makes things much easier to think about: at a minimum, if you change the body of a function it doesn't affect whether other code compiles or not. It's also one of the big differences between generic parameters (all in the function signature) and template metaprogramming (templates can do duck typing).

The obvious answer to that is then "any trait consisting only of methods which take a Self parameter". But given (a) how confusing Rust's orphan rules already are to the average programmer, and (b) how easy it is to implement your own Never type if needed, I think it's best to just have Never implement the main built-in traits (Copy, Clone, etc.) and leave it at that.

Thinking about this problem again kinda nerd-sniped me, so sharing a brain-dump here.

The first one: any type that fulfills the trait bounds set by the definer of the trait, makes sense here. If we want all associated types of ! uniformly to map a single type, the only possible choice would be !, because we are trying to define it here so that it fullfills all possible trait bounds. Another choice would be the "top" type: a generic T (module the trait bounds). Here, the type inference would give up, as it would have no information about the type, and user of the trait would need to fill in whatever type they desire in this specific type-level expression. Any other type would be kinda arbitrary, and not maximally expressive in either way.

That the user would need to select a type, is an interesting choice in the sense, that <! as Foo> would not be a valid expression in that case. It would need to be something like <! as Foo<AssocType=MyType>>, which is intriguing to me: the user of the trait would become basically an implementor of it, and passing ! to anywhere with a bounded generic type T: Foo, would instantiate not only the type T with !, but also the trait Foo with <AssocType=MyType>!

The second and the third ones: these are even tougher, as they are expressions that produce values. Rust doesn't guarantee that someone who has a type can produce a value of that type just by the virtue of having the type. But mimicking the first case, one could either imagine that they are panicking expressions of type !, which, confortably is a subtype any type, and thus any associated expression! But panicking in such cases sounds a bit awful from resiliency perspective. Another one is that again, like with the second case, the user would instantiate the trait Foo itself with <ASSOC_CONST=CONST> or <assoc_fn=func>. This would be also maximally flexible.

However, instantiating traits by setting their "parameters" is not something that Rust currently has. To be able to do that in generic code, one must also have a way to propagate such instantiated traits (e.g. from output to input). One could maybe do this without introducing "trait variables" or anything like that, by just tracking where type variables go. Still, it's a whole new consept in the already complex and hard to understand trait system.

Not even sure how it is even possible to implement every trait. Wouldn't it be the opposite? It implements no traits?

One could argue that because the bottom type is a subtype of all other types, it must to implement all the traits that any other type implements. Traits are similar to interfaces in this regard, and it's pretty clear that subtypes must implement the same interfaces their supertypes do. If not, the values of the subtype wouldn't conform to the Liskov substitution principle.

The special case of the bottom type, however, is made possible by the fact that it doesn't have values, so Liskov substitution principle is irrelevant in practice. It's pretty clear, however, that 1) it's kind of weird to do a full reversal on how subtypes work in one case (implements all the traits of the supertypes) versus others (doesn't implement any trait). 2) you want your types to be maximally flexible, so implementing more traits is good, because it allows one to use the type in more situations.

The whole point of a bottom type is that it's impossible to actually have an instance of it. It implements everything in a principle-of-explosion sort of way.

Swift has Never, which is the return type of functions that don't terminate, such as fatalError().

https://developer.apple.com/documentation/swift/never

It's currently not implemented as a bottom type in the sense that it's not the subtype of all types (discussed in https://nshipster.com/never/).

As a use case other than the bottom type or "doesn't terminate", some pure languages use it to mean "this code path is impossible". I always liked the way Elm (and I assume many other pure functional languages) define(s) `Never`:

    type Never = JustOneMore Never

As the only constructor takes an instance of itself as an argument, any attempt to construct one would become infinite.

This very naturally allows for a function to obtain any value you want:

    never : Never -> a
    never (JustOneMore nvr) =
      never nvr

If you can get a `Never` instance that can't possibly exist, you must be in a code path that can't happen, so you can get any value you want to short circuit early and make impossible return values. That makes it very useful in a language with no runtime exceptions to handle impossible cases. (E.g: you can go from a `Result Never a` to an `a` where normally you'd have to handle the error case).

[1]: https://github.com/elm/core/blob/1.0.5/src/Basics.elm#L948

Interestingly, if you read the article [0] linked in the reddit post referred to in this blog post, the author points out that the Haskell version of the bottom type has a problem - you can construct an inhabitant. Pulling out the relevant section of code:

  fix :: (a -> a) -> a      -- defined in Data.Function
  fix f = let x = f x in x  -- least fixed point of f

  false :: Void
  false = fix (id :: Void -> Void)

Since you can find an inhabitant of Void, you can therefore create an inhabitant of any type, so you can prove any proposition:

  inhabitant :: a
  inhabitant = fix id

I don't know if this is only really a problem if you were trying to use Haskell as a theorem prover. It might be the case that in practice, you're unlikely to run into this inconsistency. I think [1] provides a bit more discussion regarding this.

[0]: https://gciruelos.com/propositions-as-types.html [1]: https://frenchy64.github.io/2018/04/07/unsoundness-in-untype...

EDIT: Just found this [2] which describes the above problem in type theory language.

[2]: https://en.wikipedia.org/wiki/System_U#Girard's_paradox

Isn't this the premise of the Fast And Loose Reasoning Is Morally Correct paper, which argues that it's fine to ignore bottom when discussing program semantics? Or did I misunderstand that paper dramatically?

You also have

  error "foo" :: Void

Ultimately the issue is that Haskell programs are not guaranteed to terminate. You could write a similar function in F# too. Most (all?) theorem provers require that all functions probably terminate.

> I don't know if this is only really a problem if you were trying to use Haskell as a theorem prover.

Yes, it makes it impossible to use Haskell as anything more than a toy as far as theorem provers go. But that's OK because Haskell is not a theorem prover, it is a programming language!

This may come across as pedantic, but your example only defines a variable with the bottom type. You never actually "construct an inhabitant" because the construction itself is nonterminating. This is actually, in my experience, one of the more common uses for the bottom type - it can mark functions that never return (the "exit" function, for example, or something that loops infinitely, or something that raises an exception).

Rust actually has a type like this in addition to a bottom type (which is !). It is the Infallible type which is an enum type (a sum type) with no variants and is thus not constructible. It's purpose is to indicate that an operation always succeeds when that operation returns a Result type. But defining it that way, the compiler can use this information to remove error checks. While it doesn't implement every trait automatically, I found it to be pretty easy to implement every trait I cared about since the it just had to typecheck and not do anything useful.

`Infallible` only exists because an arbitrary empty type was needed to signal a `Result` that's always `Ok` and the "official" never type `!` was not yet implemented/stable. If it weren't for backward compatibility, `Infallible` could be removed from the standard library right now and its uses replaced with `!`.

However, `!` is not a real bottom type either, not yet anyway, because it is not the subtype of every type. As of now it is an unsolved problem how exactly one would go about making it one.

I'm not too familiar with rust's syntax -- isn't `!` normally used after identifiers to indicate macro invocation? Or is it part of the identifier that happens to name a macro?

More accurately, when I have a function that returns `!`, is that `!` a special syntax construct at the parser level, a keyword, or a name from the prelude? Or is there some special zero-name macro that is invoked? Can I put a bang in my own type name?

https://doc.rust-lang.org/reference/types/never.html seems to answer the question "it's special"

I guess the docs are: https://doc.rust-lang.org/std/primitive.never.html

> isn't `!` normally used after identifiers to indicate macro invocation?

I'm not sure where that's explicitly documented, but the docs for procedural macros call it the "macro invocation operator":

https://doc.rust-lang.org/reference/procedural-macros.html#f...

> Also, I tried searching but I couldn't find an entry for `!` in the docs.

Yeah, that's one reason I'd prefer that it had an explicit name, rather than a single character.

A special syntax construct at the parser level I think. In fact currently the `-> !` syntax for functions is it's own special syntax distinct (although v. similar in meaning) from the `!` type.

It's not a macro (macro invocations just use the same character), and you can't have a '!' in your own type names.

Yeah, in current stable Rust `-> !` is just a syntactic construct. But it is being reified into a proper first-class type [1], indeed in nightly you've been able to use it in most type positions for a while already (I actually forgot that the "basic" implementation is not yet stable!)

[1] https://github.com/rust-lang/rust/issues/35121

That's a void type, not a bottom type.

Some discussion about a rejected suggestion for a bottom type and a local hack:

  type Bottom = private Bottom of Bottom

which unfortunately

> [...] subtype of all types. My bottom type does not have this property.

I've never liked this "spinny" way if defining Void

I prefer

data Void = Void { absurd :: (forall a. a) }

This is probably a dumb question but isn't this just null by another name?

Null is a value, not a type. Think of the bottom type more like the empty set rather than the number/address zero although there are similarities to both in type theory.

It is not a dumb question. Null has many drawbacks compare to bottom types. In many languages is is part of other types so that your code happily compiles with a function that has String as an input parameter and gets a null. This is why you see in Java a lot of null checking usually. In ML languages people decided to do better and started to use Some / None, etc. which needs to be handled explicitly, so you do not forget null checking accidentally.

Well it is always a bit tricky to translate concepts between math and different programming languages, but null is a value not a type. Although null can be a member of all/many types, but I think mathematically it's more like all those types simply have a special value called 'null', look up pointed spaces.

You've also got 'void' in C which comes close, but the way I see it this is also different, in the following way:

A function f: X -> void may return, but won't return any (useful) data. Mathematically there is exactly 1 such function.

A function f: X -> Bottom does not exists, if called it is impossible for it to return.

In category theory void would be the terminal object 1 and Bottom would be the initial object 0. It's called initial because there's exactly 1 function f: Bottom -> X. In programming terms this function just crashes.

Interesting. Any tips on what to read up on to get a background on this sort of math?

A good introduction on programming language theory should get you there. You can google around for recommendations.

This falls under Category theory, but it can be a bit tricky to find a good place to start reading. It helps if you have some mathematical background on the subject, if only to know what parts are Category theory and which are restrictions of the programming language.

For example, Haskell folks seem to love to make everything about Category theory but they're not necessarily the best example since Haskell is a bit weird from a Category theory standpoint (currying isn't that natural, and is in fact a deeply abstract property that only some categories have). You'll know things have gone off the deep end when you see the word Applicative.

The C# folks tend to be a bit more down to earth with their category theory (with their contravariant / covariant type parameters and SelectMany = Monad), but they write fewer articles on category theory.

> Haskell is a bit weird from a Category theory standpoint (currying isn't that natural, and is in fact a deeply abstract property that only some categories have).

Care to expand? As far as I know, the main "weird" thing about Haskell category-theoretically is seq, which is a real pain to reason about[0], but it's strange to me that you see currying as somehow a problem.

[0]: http://math.andrej.com/2016/08/06/hask-is-not-a-category/

Well you need to dive quite deep into Category theory before you learn what exponential objects are, which are the constructs you need to have:

a -> (b -> c) ≅ (a, b) -> c

Note that the two aren't equal, merely isomorphic, but Haskell has lots of synctactic sugar that lets you pretend the two are equal.

This leads to a bit of an impedance mismatch when you throw functors in the mix, as functors are a general category theory concept and therefore do not play nice with exponential objects which only some specific categories have. This is not an insurmountable problem, but it means you suddenly need a lot more category theory to do category theory in Haskell.

Without currying as first class citizen you can just lift a function f :: (a,b) -> c as follows:

fmap f :: F (a, b) -> F c

okay you've got a tuple in your functor, but those are simple enough to deal with, however if you try this with the curried variant you get:

fmap f :: F a -> F (b -> c)

okay it takes an 'F a' as input, no surprises there, but it returns you a function wrapped in your Functor, which can be tricky to deal with as most people will expect their constructs to contain data, not functions.

You can then get to grips with this by learning about Appplicative, which you'll then find out turns your functor into a lax monoidal functor. However for someone getting to grips with category theory this is a lot to process.

Bartozs Milewski wrote a book called Category Theory for Programmers and has a series of lectures on YouTube https://www.youtube.com/user/DrBartosz

I found it to be thorough and relatively gentle (for something as abstract as category theory anyways!)

Could you please explain the difference between f: X -> void and f: X -> Bottom? If there was a void type in C, would void be Bottom?

Conceptually, void is a singleton type: it has one value. So a function which returns void does return, just without anything useful.

Bottom has no value, so a function which “returns” bottom can not terminate.

Practically, this means it either loops forever or “breaks” e.g. panics or exits the program.

No the Bottom type has no values, while the void type has exactly 1 (which doesn't have a name, but you can return it by writing `return;`).

So a function f: X -> void returns the only (nameless) value in void, depending on the programming language it will return null or equivalent or it'll just return no data (but it'll still return).

A function f: X -> Bottom is different, the type Bottom has no values so it is impossible for the function to ever return. This is not always useful, but in some strongly typed you need it to assign a value to an infinite loop.

Oh, so you have the distinction between `function foo() { return; }` and `function bar() {}`. From the languages I'm accustomed to, yes, second syntax is first syntax under the hood.

Thanks for the explanation!

> Oh, so you have the distinction between `function foo() { return; }` and `function bar() {}`. From the languages I'm accustomed to, yes, second syntax is first syntax under the hood.

The second function terminates, same as the first one, there's no real difference between them.

A bottom-returning function would be something like

    function foo() { for(;;) {} }

that genuinely never terminates and thus never exits.

No because the type bottom has no valid values, whereas null as one valid value, namely null. A function that returns bottom must loop forever, because there are no values that it would be valid for the function to return.

Loop forever, or, more commonly in actual use cases, terminate via a nonlocal return (eg. exceptions, `longjmp`, `abort`).

As an aside, in any programming language that does not support/enforce total functions, the return type `T` of any function is actually the sum type `T | Bottom`, which is to say, "this function either returns a value of type `T` or never returns to its caller at all!"

Also used as the type of expressions that do not return a value (things like `break`, `continue`, or `throw` in expression-oriented languages).

I mean, `T | Bottom` is the same type as `T`, so what you're saying is vacuously true.

Reply on news.ycombinator.com