4 ms·

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

by 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!
thedufer 6y ago
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).

by asib 6y ago

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!

thedufer 6y ago

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).