5 ms·

I don't think it's your level of abstraction, I think it's that you are treating as unrelated two sides of the same coin. This sum type / variant / disjoint uni

I don't think it's your level of abstraction, I think it's that you are treating as unrelated two sides of the same coin. This sum type / variant / disjoint union / coproduct construction operates both at the level of types and the level of values. After all, we only care about types insofar as they tell us about values.

AnimalMuppet 7y ago
So Integer (0 or 1 or 2 or...) is a sum type in the same sense that Maybe Integer (Nothing or 0 or 1 or 2 or...) is. I see. That makes some sense. So if I'm in Haskell, say, and I've got a Maybe Integer, and I'm trying to walk through the options (pattern matching), I usually see the options as Nothing or Just Integer. Can I instead do Nothing or Just 0 or... "Just some other Integer"? That is, can I treat... um, not sure how to say this in light of your post... "individual values of a particular named type" the same way as I can treat "different named types"?
- danharaj 7y ago
  Ah I see, so what you're talking about is the syntax for defining a sum type. This confused me too. In Haskell, a definition of a sum type looks something like: data MaybeInteger = Nothing | Just Integer This defines the type MaybeInteger by saying how to construct the values that inhabit it. `Nothing` is a value that is immediately of type MaybeInteger. `Just` is a way to construct a value of type MaybeInteger by feeding it an Integer. You use `Just` to construct a value by applying it to an Integer: `Just 4`, for example. There is an alternative syntax for defining sum types that might be clearer: data MaybeInteger where Nothing :: MaybeInteger Just :: Integer -> MaybeInteger When using sum types, we use a case statement: case x of Nothing -> "nothing" Just 1 -> "one" Just _ -> "something else"
  - AnimalMuppet 7y ago
    Thanks!
  - coldtea 7y ago
    data MaybeInteger where Nothing :: MaybeInteger Just :: Integer -> MaybeInteger Doesn't this mean that Nothing (ie. MaybeInteger) is the same "type"/"supertype" however you call it, as a constructor from Integer to MaybeInteger? How does that work, e.g. how does MaybeInteger is equivalent to Integer -> MaybeInteger? I guess ending up at the same type is crucial, but one looks to be the type directly, while the other a constructor for the type. And how can "Just" be a constructor for MaybeInteger here, but e.g. MaybeString in some other example? Is it specially blessed? What kind of thing it is in the language?
    - danharaj 7y ago
      Nothing and Just are constructors. Constructors need not be the same type. The whole point of a sum type is that you can construct it in multiple ways, after all. In this case Nothing is immediately a value of type MaybeInteger. Just on the other hand has the type of a function :: Integer -> MaybeInteger. So they don't have the same type, but Nothing and Just 5 have the same type, MaybeInteger. For pedagogical purposes I pretended to work with MaybeInteger instead of Maybe from Haskell. The definition of Maybe is: data Maybe a = Nothing | Just a or alternatively data Maybe a where Nothing :: Maybe a Just :: a -> Maybe a I didn't want to simultaneously explain polymorphism and sum types, but the way you can combine them is vastly more useful than either feature alone.
    - Quekid5 7y ago
      You can think of Nothing and Just as functions that construct a MaybeInteger. Nothing takes no parameters because there's no value there, so why would it? Just takes an integer and gives you a MaybeInteger containing the integer you supplied to it. There is only a single type here, namely MaybeInteger.
- WorldMaker 7y ago
  It's rarely useful (though there are some interesting examples) but it certainly is possible represent the naturals entirely in the type system as Church encodings [1] or Peano naturals [2] entirely in the Haskell type system. You'll see some references to such things elsewhere in these threads. You can have a "type" for 4 in peano naturals and use that as a type guard on a function that can only physically take the number 4, and the Haskell type checking system will enforce that. Here's one very clear implementation of Peano naturals as Haskell sum type: https://github.com/kenbot/church/blob/master/PeanoNat.hs https://github.com/kenbot/church/blob/master/PeanoNat.hs It's rare that you need that granular of a type, though, and as pointed out in sibling response it's easy enough to do with runtime pattern matching of Integer values. But it does illustrate that type abstraction "can go deeper". [1] https://en.wikipedia.org/wiki/Church_encoding https://en.wikipedia.org/wiki/Church_encoding [2] https://en.wikipedia.org/wiki/Peano_axioms https://en.wikipedia.org/wiki/Peano_axioms

AnimalMuppet 7y ago

So Integer (0 or 1 or 2 or...) is a sum type in the same sense that Maybe Integer (Nothing or 0 or 1 or 2 or...) is. I see. That makes some sense. So if I'm in Haskell, say, and I've got a Maybe Integer, and I'm trying to walk through the options (pattern matching), I usually see the options as Nothing or Just Integer. Can I instead do Nothing or Just 0 or... "Just some other Integer"? That is, can I treat... um, not sure how to say this in light of your post... "individual values of a particular named type" the same way as I can treat "different named types"?

danharaj 7y ago
Ah I see, so what you're talking about is the syntax for defining a sum type. This confused me too. In Haskell, a definition of a sum type looks something like: data MaybeInteger = Nothing | Just Integer This defines the type MaybeInteger by saying how to construct the values that inhabit it. `Nothing` is a value that is immediately of type MaybeInteger. `Just` is a way to construct a value of type MaybeInteger by feeding it an Integer. You use `Just` to construct a value by applying it to an Integer: `Just 4`, for example. There is an alternative syntax for defining sum types that might be clearer: data MaybeInteger where Nothing :: MaybeInteger Just :: Integer -> MaybeInteger When using sum types, we use a case statement: case x of Nothing -> "nothing" Just 1 -> "one" Just _ -> "something else"
- AnimalMuppet 7y ago
  Thanks!
- coldtea 7y ago
  data MaybeInteger where Nothing :: MaybeInteger Just :: Integer -> MaybeInteger Doesn't this mean that Nothing (ie. MaybeInteger) is the same "type"/"supertype" however you call it, as a constructor from Integer to MaybeInteger? How does that work, e.g. how does MaybeInteger is equivalent to Integer -> MaybeInteger? I guess ending up at the same type is crucial, but one looks to be the type directly, while the other a constructor for the type. And how can "Just" be a constructor for MaybeInteger here, but e.g. MaybeString in some other example? Is it specially blessed? What kind of thing it is in the language?
  - danharaj 7y ago
    Nothing and Just are constructors. Constructors need not be the same type. The whole point of a sum type is that you can construct it in multiple ways, after all. In this case Nothing is immediately a value of type MaybeInteger. Just on the other hand has the type of a function :: Integer -> MaybeInteger. So they don't have the same type, but Nothing and Just 5 have the same type, MaybeInteger. For pedagogical purposes I pretended to work with MaybeInteger instead of Maybe from Haskell. The definition of Maybe is: data Maybe a = Nothing | Just a or alternatively data Maybe a where Nothing :: Maybe a Just :: a -> Maybe a I didn't want to simultaneously explain polymorphism and sum types, but the way you can combine them is vastly more useful than either feature alone.
  - Quekid5 7y ago
    You can think of Nothing and Just as functions that construct a MaybeInteger. Nothing takes no parameters because there's no value there, so why would it? Just takes an integer and gives you a MaybeInteger containing the integer you supplied to it. There is only a single type here, namely MaybeInteger.
WorldMaker 7y ago
It's rarely useful (though there are some interesting examples) but it certainly is possible represent the naturals entirely in the type system as Church encodings [1] or Peano naturals [2] entirely in the Haskell type system. You'll see some references to such things elsewhere in these threads. You can have a "type" for 4 in peano naturals and use that as a type guard on a function that can only physically take the number 4, and the Haskell type checking system will enforce that. Here's one very clear implementation of Peano naturals as Haskell sum type: https://github.com/kenbot/church/blob/master/PeanoNat.hs https://github.com/kenbot/church/blob/master/PeanoNat.hs It's rare that you need that granular of a type, though, and as pointed out in sibling response it's easy enough to do with runtime pattern matching of Integer values. But it does illustrate that type abstraction "can go deeper". [1] https://en.wikipedia.org/wiki/Church_encoding https://en.wikipedia.org/wiki/Church_encoding [2] https://en.wikipedia.org/wiki/Peano_axioms https://en.wikipedia.org/wiki/Peano_axioms