6 ms·

I can never get enough of the arrow theory. Here is a malformed question that occurs to me just now: In a language like python i can form instances of a produ

I can never get enough of the arrow theory. Here is a malformed question that occurs to me just now: In a language like python i can form instances of a product type using tuples, but making instances of a sum (variant) type ... ? How is it that the duality is broken when I no longer have variable declarations? Or is every object instance already a variant (of every possible subclass) ?

tel 12y ago
"Arrow theory" here is better known as Category Theory. I highly, highly recommend learning more about it if you're interested. I cannot understate its beauty. As a starter guide, I highly recommend reading Lawvere's Conceptual Mathematics.
noelwelsh 12y ago
In a language like Python you can consider there to be one type called, say, ThePythonType, or which all types are a variant. Then all objects have type ThePythonType. A more useful type system would have "union types". They differ from sum types in that you can construct a union type from existing types in an ad-hoc manner. For example, if you have a function that returns a string or nil you can construct a union type "Union of string or nil". To do this with a sum type you'd have to have a common super type of string and nil and no other types. There are also intersection types, about which I know very little.
- seanmcdirmid 12y ago
  > In a language like Python you can consider there to be one type called, say, ThePythonType, or which all types are a variant. Then all objects have type ThePythonType. This is only if you reject the notion of a dynamic type (as most type theorists do, but programmers do not). Otherwise, Python has a rich type system that is checked at run-time. It lacks sum types, but we could easily imagine a dynamically checked realization.
  - jlouis 12y ago
    A good way of getting at this is to call things at runtime "classes" or "tags" to make it apparent that their discrimination happens at runtime, not compile-time. The problem is that if you call both things types, you quickly run into a situation where you are essentially talking about different concepts entirely. Note that most sum-types are implemented by having a runtime tag on which you can discriminate.
    - seanmcdirmid 12y ago
      Classes exist statically also. Tags are meaningless outside of implementation discussions.
  - tel 12y ago
    I don't think type theorists reject that at all. They just don't call them "types". Which I don't know why anyone would care in the context of a technical argument. If an "average programmer" here and a type theorist spent 1 minute at the beginning of the conversation normalizing terms then nobody would have any argument here. I don't think anyone tries to claim that "types" and "static types" (or, in the type theorist's parlance, "tags" and "types") are the same... they just try to argue whether or not it's "right" to call one or the other by the name "type".
    - seanmcdirmid 12y ago
      Most type theorists reject that dynamic typing is meaningful and not a misnomer, hence Noel Welsh's assertion that Python has only one type. It doesn't start the conversation off very well.
      - dllthomas 12y ago
        Did you mean that to be a restatement of what tel said? It seems to be.
        seanmcdirmid 12y ago
- dllthomas 12y ago
  "To do this with a sum type you'd have to have a common super type of string and nil and no other types." This seems wrong. You can make a new type that simply contains one of those, right? In a sense that's what you're doing with a sum type in Haskell, though there you get to produce new types automatically from higher kinded types.
- theseoafs 12y ago
  > To do this with a sum type you'd have to have a common super type of string and nil and no other types. I'm not sure you understand sum types. Sum types subsume normal unions; sum types and unions are essentially the same thing and capturing this kind of return type in Haskell or ML is extremely easy. "Supertypes" are completely unrelated and subtyping is not actually needed in languages with sum types (for example Haskell has sum types but doesn't have any real form of subtyping). For example in Haskell you'd use the `Maybe` type constructor. If your type returns a `Maybe String` that means it either returns a string or nothing.
  - dllthomas 12y ago
    You can implement a (open) sum type with supertypes, though, can't you?
    - theseoafs 12y ago
      Sort of. You can effectively do so in a language like Java, which allows you to inspect the types of objects at runtime. For example if you have a class `Foo` with two subclasses `SubA` and `SubB` you could do something like this: public static void test(Foo f) { if (f isinstanceof SubA) { SubA a = (SubA)f; /* ... */ } else if (f isinstanceof SubB) { SubB b = (SubB)f; } } This works okay but you have to implement all the machinery yourself, and for a statically typed language Java is notoriously type-unsafe so if you make a mistake with your casts you're basically not going to find out until you get an exception at runtime. And of course there might be other existing subclasses of `Foo` which means that you get no compile-time guarantee that you didn't miss a possible case. Standard ML approaches subtyping in a very different way that renders this kind of approach impossible. It gives you less freedom in that it eliminates downcasting, but that ultimately results in a safer language. Of course Standard ML has proper sum types with all of their compile-time guarantees so there's little reason for it anyway.
      - deleted 12y ago
        [deleted]
scott_s 12y ago
In object-oriented languages, I think the closest analogue to sum types are type hierarchies. It's more verbose and cumbersome, but you can get the same effect through dynamic polymorphism. Consider the example from the post: type AST = Expr of ... | Stmt of ... | Comment of ... let rec evaluate e = match e with | Expr # evaluate the ... of an Expr | Stmt # ditto | Comment # ditto In the object-oriented world, I think this most naturally maps to (forgive me for not using Python syntax; I love Python, but I rarely do much OO in it): class AST { public: virtual bool evaluate() = 0; // again, forgive the C++ syntax }; class Expr: public AST { public: virtual bool evaluate() { // Expr specific evaluate code } }; class Stmt: public AST { public: virtual bool evaluate() { // Ditto } }; class Comment: public AST { public: virtual bool evaluate() { // Ditto } }; As seanmcdirmid points out, this is not the same, as the discrimination happens at runtime. But, I think it's the closest analogue. Also note that in the algebraic data-type world, we normalize on functions. That is, what to do in order to evaluate any given AST exists in the one evaluate function. But, in the OO world, we normalize on the types; how we evaluate a given AST is spread out over the many evaluate methods.
- dllthomas 12y ago
  "As seanmcdirmid points out, this is not the same, as the discrimination happens at runtime." Doesn't the discrimination of which branch of a sum type your data represents generally happen at runtime?
  - scott_s 12y ago
    Yes. I was thinking there was an important distinction about knowing the types statically, and being able to make sure that all options have been handled. But, if in the interface you say "everyone must implement this method" (as I did), and then you don't, the compiler will issue an error in much the same way. What I was getting at is that when we use the algebraic version of AST, we know exhaustively what forms it can take. The definition tells us. In the OO version, this is note true. If we restrict our use to the polymorphic functions, then this is fine. But if we try to inspect the OO version of AST, ask its true type, and then act on it, then we may get into trouble.

tel 12y ago

"Arrow theory" here is better known as Category Theory. I highly, highly recommend learning more about it if you're interested. I cannot understate its beauty. As a starter guide, I highly recommend reading Lawvere's Conceptual Mathematics.

noelwelsh 12y ago

In a language like Python you can consider there to be one type called, say, ThePythonType, or which all types are a variant. Then all objects have type ThePythonType. A more useful type system would have "union types". They differ from sum types in that you can construct a union type from existing types in an ad-hoc manner. For example, if you have a function that returns a string or nil you can construct a union type "Union of string or nil". To do this with a sum type you'd have to have a common super type of string and nil and no other types. There are also intersection types, about which I know very little.

seanmcdirmid 12y ago
> In a language like Python you can consider there to be one type called, say, ThePythonType, or which all types are a variant. Then all objects have type ThePythonType. This is only if you reject the notion of a dynamic type (as most type theorists do, but programmers do not). Otherwise, Python has a rich type system that is checked at run-time. It lacks sum types, but we could easily imagine a dynamically checked realization.
- jlouis 12y ago
  A good way of getting at this is to call things at runtime "classes" or "tags" to make it apparent that their discrimination happens at runtime, not compile-time. The problem is that if you call both things types, you quickly run into a situation where you are essentially talking about different concepts entirely. Note that most sum-types are implemented by having a runtime tag on which you can discriminate.
  - seanmcdirmid 12y ago
    Classes exist statically also. Tags are meaningless outside of implementation discussions.
- tel 12y ago
  I don't think type theorists reject that at all. They just don't call them "types". Which I don't know why anyone would care in the context of a technical argument. If an "average programmer" here and a type theorist spent 1 minute at the beginning of the conversation normalizing terms then nobody would have any argument here. I don't think anyone tries to claim that "types" and "static types" (or, in the type theorist's parlance, "tags" and "types") are the same... they just try to argue whether or not it's "right" to call one or the other by the name "type".
  - seanmcdirmid 12y ago
    Most type theorists reject that dynamic typing is meaningful and not a misnomer, hence Noel Welsh's assertion that Python has only one type. It doesn't start the conversation off very well.
    - dllthomas 12y ago
      Did you mean that to be a restatement of what tel said? It seems to be.
      - seanmcdirmid 12y ago
dllthomas 12y ago
"To do this with a sum type you'd have to have a common super type of string and nil and no other types." This seems wrong. You can make a new type that simply contains one of those, right? In a sense that's what you're doing with a sum type in Haskell, though there you get to produce new types automatically from higher kinded types.
theseoafs 12y ago
> To do this with a sum type you'd have to have a common super type of string and nil and no other types. I'm not sure you understand sum types. Sum types subsume normal unions; sum types and unions are essentially the same thing and capturing this kind of return type in Haskell or ML is extremely easy. "Supertypes" are completely unrelated and subtyping is not actually needed in languages with sum types (for example Haskell has sum types but doesn't have any real form of subtyping). For example in Haskell you'd use the `Maybe` type constructor. If your type returns a `Maybe String` that means it either returns a string or nothing.
- dllthomas 12y ago
  You can implement a (open) sum type with supertypes, though, can't you?
  - theseoafs 12y ago
    Sort of. You can effectively do so in a language like Java, which allows you to inspect the types of objects at runtime. For example if you have a class `Foo` with two subclasses `SubA` and `SubB` you could do something like this: public static void test(Foo f) { if (f isinstanceof SubA) { SubA a = (SubA)f; /* ... */ } else if (f isinstanceof SubB) { SubB b = (SubB)f; } } This works okay but you have to implement all the machinery yourself, and for a statically typed language Java is notoriously type-unsafe so if you make a mistake with your casts you're basically not going to find out until you get an exception at runtime. And of course there might be other existing subclasses of `Foo` which means that you get no compile-time guarantee that you didn't miss a possible case. Standard ML approaches subtyping in a very different way that renders this kind of approach impossible. It gives you less freedom in that it eliminates downcasting, but that ultimately results in a safer language. Of course Standard ML has proper sum types with all of their compile-time guarantees so there's little reason for it anyway.
    - deleted 12y ago
      [deleted]

scott_s 12y ago

In object-oriented languages, I think the closest analogue to sum types are type hierarchies. It's more verbose and cumbersome, but you can get the same effect through dynamic polymorphism. Consider the example from the post: type AST = Expr of ... | Stmt of ... | Comment of ... let rec evaluate e = match e with | Expr # evaluate the ... of an Expr | Stmt # ditto | Comment # ditto In the object-oriented world, I think this most naturally maps to (forgive me for not using Python syntax; I love Python, but I rarely do much OO in it): class AST { public: virtual bool evaluate() = 0; // again, forgive the C++ syntax }; class Expr: public AST { public: virtual bool evaluate() { // Expr specific evaluate code } }; class Stmt: public AST { public: virtual bool evaluate() { // Ditto } }; class Comment: public AST { public: virtual bool evaluate() { // Ditto } }; As seanmcdirmid points out, this is not the same, as the discrimination happens at runtime. But, I think it's the closest analogue. Also note that in the algebraic data-type world, we normalize on functions. That is, what to do in order to evaluate any given AST exists in the one evaluate function. But, in the OO world, we normalize on the types; how we evaluate a given AST is spread out over the many evaluate methods.

dllthomas 12y ago
"As seanmcdirmid points out, this is not the same, as the discrimination happens at runtime." Doesn't the discrimination of which branch of a sum type your data represents generally happen at runtime?
- scott_s 12y ago
  Yes. I was thinking there was an important distinction about knowing the types statically, and being able to make sure that all options have been handled. But, if in the interface you say "everyone must implement this method" (as I did), and then you don't, the compiler will issue an error in much the same way. What I was getting at is that when we use the algebraic version of AST, we know exhaustively what forms it can take. The definition tells us. In the OO version, this is note true. If we restrict our use to the polymorphic functions, then this is fine. But if we try to inspect the OO version of AST, ask its true type, and then act on it, then we may get into trouble.