5 ms·

The following has always had me a bit puzzled, be interested in responses. If bottom type corresponds to no(thing) and top to any(thing) where does every(thing

The following has always had me a bit puzzled, be interested in responses. If bottom type corresponds to no(thing) and top to any(thing) where does every(thing) and some(thing) fit in? Is there any semantic distinction between any(thing) and every(thing)? There should be, right? For me, some(thing) that had type any(thing) would be an _individual_ but some(thing) that had type every(thing) {actually the mind boggles a bit here} would be a _colection_, the collection of all existing or living things. In fact Ruby has the notion of Objectspace. So we can say things like ObjectSpace.each_object{|x| p x}

junke 11y ago
The any type is an "or" of all your types. Any value in your type system belongs to the top type. The bottom type is a type for which no existing value belongs to this type. What would an "everything" type be? I'd guess the "and" of all your types, meaning "any value that belongs to all (non-bottom?) types" (e.g. an imaginary 0 symbol meaning zero float, empty list, empty string according to the context). If you want your "every" type to consider bottom type, then the intersection is empty. Likewise, the "some" type would be a type containing values that belong to at least one type, which IMO looks like the "any" type.
- AnimalMuppet 11y ago
  An "everthing" type is impossible. It would not only have to be a float, a list, a string, but also a tuple, a monad, and everything else. So 0 might work as an empty string, and 1 might work as a string, but 1 wouldn't work as a dictionary at all, or as a monad, or...
  - junke 11y ago
    In that case the everything type is just bottom. (edit: to be clear, the bottom type, aka zero/empty type).
    - igravious 11y ago
      But bottom is "nothing" and how can "everything" be "nothing"? But then again, should "everything" contain (is that even the right word?) all things, each and every thing, including "nothing"?
      - lmkg 11y ago
        "Everything" is the intersection of all types (rather than the union, which is "Anything"). It does not means that it contains the values that all types contain. Rather, it contains the values that belong to every type. In other words, in order to belong to the type "Everything," a value has to simultaneously belong to every other type. One way to think about this is that the name applies to each member of the type, not to the type as a whole. "Anything" is an accurate description of any possible value, so the set contains all values. "Everything" does not apply to the entire set, but to each individual element. An element must be everything all at once in order for us to describe it as "Everything." Nothing does that, so "Nothing" does that.
        catnaroek 11y ago
        This confusion is why explicitly using logical quantifiers is preferable: `exists x. x` is (isomorphic to) the top type (if there is one), and `forall x. x` is (isomorphic to) the bottom type (if there is one). Avoid natural language like the plague.
    - pklausler 11y ago
      Bottom's not a type; it's a value that inhabits all types.
      - catnaroek 11y ago
        Some type systems also have a bottom type, and this has nothing to do with the bottom you're talking about.
      - gclaramunt 11y ago
        If you consider subtyping, Bottom is a type IIRC, In the category with types as objects and subtyping relationship (a->b if b is subtype of a) as morphisms, Any is the initial object and Bottom is the final object of the category
  - tel 11y ago
    Well, existential types are pretty similar. If you've got (exists a . a) then you have to be prepared for it to be a float, but also prepared for it to be a list, or a string, but also a tuple, some type for which we only know that it is a monad, and everything else :) More specifically, we've lost any information to tell us what specific thing might be here so we have to be prepared for any answer. It's the inverse of (forall a . a) which we can ask to become whatever we like.
- igravious 11y ago
  Yes, I've seen Any (or top) described like that. It is the super-type of all types. Therefore, as you say, "Any value in your type system belongs to the top type". Imagine the following: foo = Sheep.new => a sheep foo.is_a(Any) => true (for anything! by the nature of Any) I agree that "some" looks like "any". I wonder is there any (ahem) semantic difference in the context we are considering. I can see why you would say that (every)thing is the "and" of all my types. But consider that I think it obvious that (every)thing should cover all things, this would include instantiations of types as well as the types themselves. Programming environment-wise I'm having a hard time imagining how "everything" would work. It must be related to for_all or universal quantification somehow...
  - jerf 11y ago
    "Programming environment-wise I'm having a hard time imagining how "everything" would work." It may be worth taking a moment to skip out on the abstraction and look more at the representation layer. In the general case, in most if not all implementations, "Any" basically translates to a "Variant" type: https://en.wikipedia.org/wiki/Variant_type https://en.wikipedia.org/wiki/Variant_type "Dynamically-typed languages" are basically those languages where all variables have the type Any. (The values generally have specific types, but the variables are all Any.)
  - junke 11y ago
    > But consider that I think it obvious that (every)thing should cover all things, this would include instantiations of types as well as the types themselves. Types are there to describe the values that can be manipulated by your program. So "as well as the types themselves" is only a concern if your language can manipulate types as first-class values. And this is not so different from all the other types in your language, at this point. What property should a value hold to belong to the "everything" type, then?
kailuowang 11y ago
I think you are thinking a group of things as a group of types. Those two concepts are separate. A group of things has its own type which is not necessarily related to the type of the things in that group. If you want an Everything type that is different from the Any type, the only type I can think of would be a type whose instances behave the same as every type. That doesn't make a lot sense to me.
- igravious 11y ago
  > If you want an Everything type that is different from the Any type, the only type I can think of would be a type whose instances behave the same as every type. That doesn't make a lot sense to me. I know, right? For me, everything semantically would have to include all types and all instances of types. Types are things also after all. In type theory collections of types are called universes. I'm not referring to those (I think). Everything encompasses all things, not just all types. Also, would everything include itself? Giving us Russell's paradox, which type theory seeks to avoid. We ought to be able to talk about all things. And everything is an alias for the phrase "all things". I agree that Any is kind of (exactly) like void* in C or BasicObject in Ruby.
  - junke 11y ago
    Well, I understand what you mean with void* but as a type, void* is not a supertype of all other types.
CuriousSkeptic 11y ago
You might enjoy this exchange on the topic https://groups.google.com/forum/m/#!msg/scala-debate/vysv97J0xok/WV8ygY4usqkJ https://groups.google.com/forum/m/#!msg/scala-debate/vysv97J...
lmm 11y ago
One of the reasons we need these precise terms is that English is imprecise, and inadequate for this sort of thing. A more useful analogy is the one with formal logic, which can be made precise (Curry-Howard). I'd advise looking that up if you're interested in this sort of thing. To sort-of approach your questions, ideas that you might find interesting are an unbound existential type T forSome { type T }, and also the fact that Nothing <: T for any type T (this is the principle of explosion in logic)

junke 11y ago

The any type is an "or" of all your types. Any value in your type system belongs to the top type. The bottom type is a type for which no existing value belongs to this type. What would an "everything" type be? I'd guess the "and" of all your types, meaning "any value that belongs to all (non-bottom?) types" (e.g. an imaginary 0 symbol meaning zero float, empty list, empty string according to the context). If you want your "every" type to consider bottom type, then the intersection is empty. Likewise, the "some" type would be a type containing values that belong to at least one type, which IMO looks like the "any" type.

AnimalMuppet 11y ago
An "everthing" type is impossible. It would not only have to be a float, a list, a string, but also a tuple, a monad, and everything else. So 0 might work as an empty string, and 1 might work as a string, but 1 wouldn't work as a dictionary at all, or as a monad, or...
- junke 11y ago
  In that case the everything type is just bottom. (edit: to be clear, the bottom type, aka zero/empty type).
  - igravious 11y ago
    But bottom is "nothing" and how can "everything" be "nothing"? But then again, should "everything" contain (is that even the right word?) all things, each and every thing, including "nothing"?
    - lmkg 11y ago
      "Everything" is the intersection of all types (rather than the union, which is "Anything"). It does not means that it contains the values that all types contain. Rather, it contains the values that belong to every type. In other words, in order to belong to the type "Everything," a value has to simultaneously belong to every other type. One way to think about this is that the name applies to each member of the type, not to the type as a whole. "Anything" is an accurate description of any possible value, so the set contains all values. "Everything" does not apply to the entire set, but to each individual element. An element must be everything all at once in order for us to describe it as "Everything." Nothing does that, so "Nothing" does that.
      - catnaroek 11y ago
        This confusion is why explicitly using logical quantifiers is preferable: `exists x. x` is (isomorphic to) the top type (if there is one), and `forall x. x` is (isomorphic to) the bottom type (if there is one). Avoid natural language like the plague.
  - pklausler 11y ago
    Bottom's not a type; it's a value that inhabits all types.
    - catnaroek 11y ago
      Some type systems also have a bottom type, and this has nothing to do with the bottom you're talking about.
    - gclaramunt 11y ago
      If you consider subtyping, Bottom is a type IIRC, In the category with types as objects and subtyping relationship (a->b if b is subtype of a) as morphisms, Any is the initial object and Bottom is the final object of the category
- tel 11y ago
  Well, existential types are pretty similar. If you've got (exists a . a) then you have to be prepared for it to be a float, but also prepared for it to be a list, or a string, but also a tuple, some type for which we only know that it is a monad, and everything else :) More specifically, we've lost any information to tell us what specific thing might be here so we have to be prepared for any answer. It's the inverse of (forall a . a) which we can ask to become whatever we like.
igravious 11y ago
Yes, I've seen Any (or top) described like that. It is the super-type of all types. Therefore, as you say, "Any value in your type system belongs to the top type". Imagine the following: foo = Sheep.new => a sheep foo.is_a(Any) => true (for anything! by the nature of Any) I agree that "some" looks like "any". I wonder is there any (ahem) semantic difference in the context we are considering. I can see why you would say that (every)thing is the "and" of all my types. But consider that I think it obvious that (every)thing should cover all things, this would include instantiations of types as well as the types themselves. Programming environment-wise I'm having a hard time imagining how "everything" would work. It must be related to for_all or universal quantification somehow...
- jerf 11y ago
  "Programming environment-wise I'm having a hard time imagining how "everything" would work." It may be worth taking a moment to skip out on the abstraction and look more at the representation layer. In the general case, in most if not all implementations, "Any" basically translates to a "Variant" type: https://en.wikipedia.org/wiki/Variant_type https://en.wikipedia.org/wiki/Variant_type "Dynamically-typed languages" are basically those languages where all variables have the type Any. (The values generally have specific types, but the variables are all Any.)
- junke 11y ago
  > But consider that I think it obvious that (every)thing should cover all things, this would include instantiations of types as well as the types themselves. Types are there to describe the values that can be manipulated by your program. So "as well as the types themselves" is only a concern if your language can manipulate types as first-class values. And this is not so different from all the other types in your language, at this point. What property should a value hold to belong to the "everything" type, then?

kailuowang 11y ago

I think you are thinking a group of things as a group of types. Those two concepts are separate. A group of things has its own type which is not necessarily related to the type of the things in that group. If you want an Everything type that is different from the Any type, the only type I can think of would be a type whose instances behave the same as every type. That doesn't make a lot sense to me.

igravious 11y ago
> If you want an Everything type that is different from the Any type, the only type I can think of would be a type whose instances behave the same as every type. That doesn't make a lot sense to me. I know, right? For me, everything semantically would have to include all types and all instances of types. Types are things also after all. In type theory collections of types are called universes. I'm not referring to those (I think). Everything encompasses all things, not just all types. Also, would everything include itself? Giving us Russell's paradox, which type theory seeks to avoid. We ought to be able to talk about all things. And everything is an alias for the phrase "all things". I agree that Any is kind of (exactly) like void* in C or BasicObject in Ruby.
- junke 11y ago
  Well, I understand what you mean with void* but as a type, void* is not a supertype of all other types.

CuriousSkeptic 11y ago

You might enjoy this exchange on the topic https://groups.google.com/forum/m/#!msg/scala-debate/vysv97J0xok/WV8ygY4usqkJ https://groups.google.com/forum/m/#!msg/scala-debate/vysv97J...

lmm 11y ago

One of the reasons we need these precise terms is that English is imprecise, and inadequate for this sort of thing. A more useful analogy is the one with formal logic, which can be made precise (Curry-Howard). I'd advise looking that up if you're interested in this sort of thing. To sort-of approach your questions, ideas that you might find interesting are an unbound existential type T forSome { type T }, and also the fact that Nothing <: T for any type T (this is the principle of explosion in logic)