14 ms·

Bottom Type in F#

55 points by adelarsq 6y ago

karmakaze 6y ago
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.
slaymaker1907 6y ago
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.
- Sharlin 6y ago
  `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.
  - EE84M3i 6y ago
    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 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 https://doc.rust-lang.org/std/primitive.never.html
    - DougBTX 6y ago
      > 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#function-like-procedural-macros 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.
    - nicoburns 6y ago
      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.
      - Sharlin 6y ago
        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 https://github.com/rust-lang/rust/issues/35121
- vmchale 6y ago
  That's a void type, not a bottom type.
mlex 6y ago
Swift has Never, which is the return type of functions that don't terminate, such as fatalError(). https://developer.apple.com/documentation/swift/never 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/ https://nshipster.com/never/).
- Latty 6y ago
  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 https://github.com/elm/core/blob/1.0.5/src/Basics.elm#L948
xupybd 6y ago
This is probably a dumb question but isn't this just null by another name?
- guerrilla 6y ago
  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.
  - draw_down 6y ago
    In some languages null is the value and the name of the type, JS for example.
- StreamBright 6y ago
  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.
- contravariant 6y ago
  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.
tegeek 6y ago
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 type JsonValue = | String of string | Number of decimal | Float of float | Record of properties:(string * JsonValue)[] | Array of elements:JsonValue[] | Boolean of bool | Null Then everything starts from here.
- bsaul 6y ago
  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.
  - GiorgioG 6y ago
    > 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.
    - nwsm 6y ago
      However, I would be interested in server-side Swift if anyone has good use cases or resources.
    - bsaul 6y ago
      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.
asib 6y ago
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 https://gciruelos.com/propositions-as-types.html [1]: https://frenchy64.github.io/2018/04/07/unsoundness-in-untyped-types.html 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 https://en.wikipedia.org/wiki/System_U#Girard's_paradox
- kqr 6y ago
  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?
- dan-robertson 6y ago
  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.
- tome 6y ago
  > 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!
- 6y ago
GolDDranks 6y ago
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.
- lmm 6y ago
  > 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.
  - GolDDranks 6y ago
    Then you might get logical inconsistencies with traits that are designed to be mutually exclusive and are used in type-level programming.
    - Joker_vD 6y ago
      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/unsound-oopsla16.pdf https://raw.githubusercontent.com/namin/unsound/master/doc/u...
  - Sharlin 6y ago
    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.
whateveracct 6y ago
I've never liked this "spinny" way if defining Void I prefer data Void = Void { absurd :: (forall a. a) }

55 points by adelarsq 6y ago

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.

slaymaker1907 6y ago

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.

Sharlin 6y ago
`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.
- EE84M3i 6y ago
  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 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 https://doc.rust-lang.org/std/primitive.never.html
  - DougBTX 6y ago
    > 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#function-like-procedural-macros 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.
  - nicoburns 6y ago
    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.
    - Sharlin 6y ago
      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 https://github.com/rust-lang/rust/issues/35121
vmchale 6y ago
That's a void type, not a bottom type.

mlex 6y ago

Swift has Never, which is the return type of functions that don't terminate, such as fatalError(). https://developer.apple.com/documentation/swift/never 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/ https://nshipster.com/never/).

Latty 6y ago
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 https://github.com/elm/core/blob/1.0.5/src/Basics.elm#L948

xupybd 6y ago

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

guerrilla 6y ago
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.
- draw_down 6y ago
  In some languages null is the value and the name of the type, JS for example.
StreamBright 6y ago
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.
contravariant 6y ago
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.

tegeek 6y ago

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 type JsonValue = | String of string | Number of decimal | Float of float | Record of properties:(string * JsonValue)[] | Array of elements:JsonValue[] | Boolean of bool | Null Then everything starts from here.

bsaul 6y ago
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.
- GiorgioG 6y ago
  > 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.
  - nwsm 6y ago
    However, I would be interested in server-side Swift if anyone has good use cases or resources.
  - bsaul 6y ago
    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.

asib 6y ago

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 https://gciruelos.com/propositions-as-types.html [1]: https://frenchy64.github.io/2018/04/07/unsoundness-in-untyped-types.html 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 https://en.wikipedia.org/wiki/System_U#Girard's_paradox

kqr 6y ago
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?
dan-robertson 6y ago
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.
tome 6y ago
> 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!
6y ago

GolDDranks 6y ago

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.

lmm 6y ago
> 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.
- GolDDranks 6y ago
  Then you might get logical inconsistencies with traits that are designed to be mutually exclusive and are used in type-level programming.
  - Joker_vD 6y ago
    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/unsound-oopsla16.pdf https://raw.githubusercontent.com/namin/unsound/master/doc/u...
- Sharlin 6y ago
  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.

whateveracct 6y ago

I've never liked this "spinny" way if defining Void I prefer data Void = Void { absurd :: (forall a. a) }