On 07/08/2017 10:25 PM, Walter Bright wrote:
On 7/8/2017 7:01 PM, sarn wrote:
On Sunday, 9 July 2017 at 00:16:50 UTC, Walter Bright wrote:
We have types that cannot be named (Voldemort types), types that have
no type (void), I suppose that types that cannot exist will fill out
the edge cases of the menagerie.
I assume there is a standard jargon for this - does anyone know Type
Theory?
Are there any other interesting uses for a type that cannot exist?
In pure functional languages, that's what "bottom" or Haskell's Void is.
In Curry–Howard "programs are proofs" theory, a type is a proposition
and an instance is a proof. A type with no instance is a proposition
that can't be proved.
https://codewords.recurse.com/issues/one/type-systems-and-logic
I'm not sure how much impact this has on everyday D programming, but
hey, it's a thing.
Thanks, it looks like we won't get any help from type theory. We're on
our own :-)
How does the information provided lead to such a conclusion? There's
established theory and practice on that.
https://en.wikipedia.org/wiki/Bottom_type
The "Bottom" type (bottom of the type hierarchy lattice) is what's
needed. If "Object" is the total set i.e. the top of the lattice i.e.
the type that is so general all types are a subset of it, then "Bottom"
is the type that is a subtype of all types and is so particular it can't
be even instantiated. It implicitly converts to everything because it's
a subtype of everything. Obviously conversion doesn't need to be honored
because the function never returns.
Andrei
