Re: [Haskell-cafe] Musings on type systems
On 20/11/2010 08:42 AM, Tillmann Rendel wrote: Hi Andrew, Andrew Coppin wrote: Now, what about type variables? What do they do? Well now, that seems to be slightly interesting, since a type variable holds an entire type (whereas normal program variables just hold a single value), and each occurrance of the same variable is statically guaranteed to hold the same thing at all times. It's sort of like how every instance of a normal program variable holds the same value, except that you don't explicitly say what that value is; the compiler infers it. What do you mean by hold the same thing at all times? Consider the following program: id :: forall a . a - a id x = x call1 :: Bool call1 = id True call2 :: Int call2 = id 42 This program contains a type variable a, and a value variable x. Now, these variables do *not* mean the same thing at all times. In the first call of id, a is Bool and x is True; but in the second call of id, a is Int and x is 42. If these variables would mean the same thing at all times, I would expect them to be called constants, wouldn't you? That would be why I said instance of a variable, rather than variable. (There's also the alpha conversion problem, for example.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
On 11/20/10 6:33 AM, Ketil Malde wrote: Andrew Coppinandrewcop...@btinternet.com writes: Now here's an interesting thought. Haskell has algebraic data types. Algebraic because they are sum types of product types (or, equivilently, product types of sum types). Now I don't actually know what those terms mean, The quick rule to remember this that the size of the resulting types correspond to the arithmetic names. I.e. data Sum a b = A a | B b -- values = values in a + values in b data Prod a b = P a b-- values = values in a * values in b I guess this makes [X] an exponential type, although I don't remember seeing that term :-) Nope. (a-b) is the exponential type, namely |a-b| = |b|^|a|. [_] is just a solution to the recursive equation [x] = 1 + x*[x]. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
On 21/11/2010 8:33 PM, wren ng thornton wrote: On 11/20/10 6:33 AM, Ketil Malde wrote: I guess this makes [X] an exponential type, although I don't remember seeing that term :-) Nope. (a-b) is the exponential type, namely |a-b| = |b|^|a|. [_] is just a solution to the recursive equation [x] = 1 + x*[x]. So that [X] correspond to the 'type' 1/(1-X). This is sometimes called the 'asterate' in other contexts, since it corresponds to the Kleene star. The nice thing about the 'asterate' is that it exists for many many semi-rings -- and one can use it as a replacement for both 'minus' and 'exact division' in the Gaussian Elimination algorithm. Jacques ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
Hi Andrew, Andrew Coppin wrote: Now, what about type variables? What do they do? Well now, that seems to be slightly interesting, since a type variable holds an entire type (whereas normal program variables just hold a single value), and each occurrance of the same variable is statically guaranteed to hold the same thing at all times. It's sort of like how every instance of a normal program variable holds the same value, except that you don't explicitly say what that value is; the compiler infers it. What do you mean by hold the same thing at all times? Consider the following program: id :: forall a . a - a id x = x call1 :: Bool call1 = id True call2 :: Int call2 = id 42 This program contains a type variable a, and a value variable x. Now, these variables do *not* mean the same thing at all times. In the first call of id, a is Bool and x is True; but in the second call of id, a is Int and x is 42. If these variables would mean the same thing at all times, I would expect them to be called constants, wouldn't you? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
Andrew Coppin andrewcop...@btinternet.com writes: Now here's an interesting thought. Haskell has algebraic data types. Algebraic because they are sum types of product types (or, equivilently, product types of sum types). Now I don't actually know what those terms mean, The quick rule to remember this that the size of the resulting types correspond to the arithmetic names. I.e. data Sum a b = A a | B b -- values = values in a + values in b data Prod a b = P a b-- values = values in a * values in b I guess this makes [X] an exponential type, although I don't remember seeing that term :-) -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
Ketil Malde wrote: data Sum a b = A a | B b -- values = values in a + values in b data Prod a b = P a b-- values = values in a * values in b I guess this makes [X] an exponential type, although I don't remember seeing that term :-) I would expect the exponential type to be (a - b): type Exp b a = a - b -- values = values in b ^ values in a Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
On 20 November 2010 12:05, Tillmann Rendel ren...@mathematik.uni-marburg.de wrote: I would expect the exponential type to be (a - b): Terminologically, Bananas in Space (!) agrees with you. http://www.cs.nott.ac.uk/~gmh/bananas.pdf Regards Stephen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Musings on type systems
OK, so how do types actually work? Musing on this for a moment, it seems that declaring a variable to have a certain type constrains the possible values that the variable can have. You could say that a type is some sort of set, and that by issuing a type declaration, the compiler statically guarantees that the variable's value will always be an element of this set. Now here's an interesting thought. Haskell has algebraic data types. Algebraic because they are sum types of product types (or, equivilently, product types of sum types). Now I don't actually know what those terms mean, but proceeding by logical inferrence, it seems that Either X Y defines a set that could be described as the union or sum of the types X and Y. So is Either what is meant by a sum type? Similarly, (X, Y) is a set that could be considered the Cartesian product of the sets X and Y. It even has product in the name. So is this a product type? So not only do we have types which denote sets of possible values, but we have operators for constructing new sets from existing ones. (Mostly just applying type constructors to arguments.) Notionally (-) is just another type constructor, so functions aren't fundamentally different to any other types - at least, as far as the type system goes. Now, what about type variables? What do they do? Well now, that seems to be slightly interesting, since a type variable holds an entire type (whereas normal program variables just hold a single value), and each occurrance of the same variable is statically guaranteed to hold the same thing at all times. It's sort of like how every instance of a normal program variable holds the same value, except that you don't explicitly say what that value is; the compiler infers it. So what about classes? Well, restricting ourselves to single-parameter classes, it seems to me that a class is like a *set of types*. Now, interestingly, an enumeration type is a set of values where you explicitly list all possible values. But once defined, it is impossible to add new values to the set. You could say this is a closed set. A type, on the other hand, is an open set of types; you can add new types at any time. I honestly can't think of a useful intuition for MPTCs right now. Now what happens if you add associated types? For example, the canonical class Container c where type Element c :: * We already have type constructor functions such as Maybe with takes a type and constructs a new type. But here we seem to have a general function, Element, which takes some type and returns a new, arbitrary, type. And we define it by a series of equations: instance Container [x] where Element [x] = x instance Container ByteString where Element ByteString = Word8 instance (Ord x) = Container (Set x) where Element (Set x) = x instance Container IntSet where Element IntSet = Int ... Further, the inputs to this function are statically guaranteed to be types from the set (class) Container. So it's /almost/ like a regular value-level function, just with weird definition syntax. Where *the hell* do GADTs fit in here? Well, they're usually used with phantom types, so I guess we need to figure out where phantom types fit in. To the type checker, Foo Int and Foo Bool are two totally seperate types. In the phantom type case, the set of possible values for both types are actually identical. So really we just have two names for the same set. The same thing goes for a type alias (the type keyword). It's not quite the same as a newtype, since then the value expressions do actually change. So it seems that a GADT is an ADT where the elements of the set are assigned to sets of different names, or the elements are partitioned into disjoint sets with different names. Hmm, interesting. At the same type, values have types, and types have kinds. As best as I can tell, kinds exist only to distinguish between /types/ and /type functions/. For type constructors, this is the whole story. But for associated types, it's more complicated. For example, Element :: * - *, however the type argument is statically guaranteed to belong to the Container set (class). In other news... my head hurts! _ So what would happen if some crazy person decided to make the kind system more like the type system? Or make the type system more like the value system? Do we end up with another layer to our cake? Is it possible to generalise it to an infinite number of layers? Or to a circular hierachy? Is any of this /useful/ in any way? Have aliens contacted Earth in living member? OK, I should probably stop typing now. [So you see what I did there?] Also, I have a sinking feeling that if anybody actually replies to this email, I'm not going to comprehend a single word of what they're talking about... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org
Re: [Haskell-cafe] Musings on type systems
There's a lot of interesting material on this stuff if you start poking around :) http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ might be a good introduction. I'd consider typeclasses to be sets of types, as you said, but more generally, a relation of types. In that view, an MPTC is just an n-ary relation over types. Yes, you can get arbitrarily deep on the hierarchy of types and kinds. Agda does this, and even lets you define things that are polymorphic on the universe level. If you do read through TTFP, you might want to follow along with Agda, as it fits quite nicely. On Fri, Nov 19, 2010 at 4:05 PM, Andrew Coppin andrewcop...@btinternet.comwrote: OK, so how do types actually work? Musing on this for a moment, it seems that declaring a variable to have a certain type constrains the possible values that the variable can have. You could say that a type is some sort of set, and that by issuing a type declaration, the compiler statically guarantees that the variable's value will always be an element of this set. Now here's an interesting thought. Haskell has algebraic data types. Algebraic because they are sum types of product types (or, equivilently, product types of sum types). Now I don't actually know what those terms mean, but proceeding by logical inferrence, it seems that Either X Y defines a set that could be described as the union or sum of the types X and Y. So is Either what is meant by a sum type? Similarly, (X, Y) is a set that could be considered the Cartesian product of the sets X and Y. It even has product in the name. So is this a product type? So not only do we have types which denote sets of possible values, but we have operators for constructing new sets from existing ones. (Mostly just applying type constructors to arguments.) Notionally (-) is just another type constructor, so functions aren't fundamentally different to any other types - at least, as far as the type system goes. Now, what about type variables? What do they do? Well now, that seems to be slightly interesting, since a type variable holds an entire type (whereas normal program variables just hold a single value), and each occurrance of the same variable is statically guaranteed to hold the same thing at all times. It's sort of like how every instance of a normal program variable holds the same value, except that you don't explicitly say what that value is; the compiler infers it. So what about classes? Well, restricting ourselves to single-parameter classes, it seems to me that a class is like a *set of types*. Now, interestingly, an enumeration type is a set of values where you explicitly list all possible values. But once defined, it is impossible to add new values to the set. You could say this is a closed set. A type, on the other hand, is an open set of types; you can add new types at any time. I honestly can't think of a useful intuition for MPTCs right now. Now what happens if you add associated types? For example, the canonical class Container c where type Element c :: * We already have type constructor functions such as Maybe with takes a type and constructs a new type. But here we seem to have a general function, Element, which takes some type and returns a new, arbitrary, type. And we define it by a series of equations: instance Container [x] where Element [x] = x instance Container ByteString where Element ByteString = Word8 instance (Ord x) = Container (Set x) where Element (Set x) = x instance Container IntSet where Element IntSet = Int ... Further, the inputs to this function are statically guaranteed to be types from the set (class) Container. So it's /almost/ like a regular value-level function, just with weird definition syntax. Where *the hell* do GADTs fit in here? Well, they're usually used with phantom types, so I guess we need to figure out where phantom types fit in. To the type checker, Foo Int and Foo Bool are two totally seperate types. In the phantom type case, the set of possible values for both types are actually identical. So really we just have two names for the same set. The same thing goes for a type alias (the type keyword). It's not quite the same as a newtype, since then the value expressions do actually change. So it seems that a GADT is an ADT where the elements of the set are assigned to sets of different names, or the elements are partitioned into disjoint sets with different names. Hmm, interesting. At the same type, values have types, and types have kinds. As best as I can tell, kinds exist only to distinguish between /types/ and /type functions/. For type constructors, this is the whole story. But for associated types, it's more complicated. For example, Element :: * - *, however the type argument is statically guaranteed to belong to the Container set (class). In other news... my head hurts! _ So what would happen if some crazy person decided to make the kind system more like
Re: [Haskell-cafe] Musings on type systems
TAPL is also a great book for getting up to speed on type theory: http://www.cis.upenn.edu/~bcpierce/tapl/ I am no type theorist, and I nonetheless found it very approachable. I've never read TTFP; I will have to check that out. (-: On Nov 19, 2010, at 4:31 PM, Daniel Peebles wrote: There's a lot of interesting material on this stuff if you start poking around :) http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ might be a good introduction. I'd consider typeclasses to be sets of types, as you said, but more generally, a relation of types. In that view, an MPTC is just an n-ary relation over types. Yes, you can get arbitrarily deep on the hierarchy of types and kinds. Agda does this, and even lets you define things that are polymorphic on the universe level. If you do read through TTFP, you might want to follow along with Agda, as it fits quite nicely. On Fri, Nov 19, 2010 at 4:05 PM, Andrew Coppin andrewcop...@btinternet.com wrote: OK, so how do types actually work? Musing on this for a moment, it seems that declaring a variable to have a certain type constrains the possible values that the variable can have. You could say that a type is some sort of set, and that by issuing a type declaration, the compiler statically guarantees that the variable's value will always be an element of this set. Now here's an interesting thought. Haskell has algebraic data types. Algebraic because they are sum types of product types (or, equivilently, product types of sum types). Now I don't actually know what those terms mean, but proceeding by logical inferrence, it seems that Either X Y defines a set that could be described as the union or sum of the types X and Y. So is Either what is meant by a sum type? Similarly, (X, Y) is a set that could be considered the Cartesian product of the sets X and Y. It even has product in the name. So is this a product type? So not only do we have types which denote sets of possible values, but we have operators for constructing new sets from existing ones. (Mostly just applying type constructors to arguments.) Notionally (-) is just another type constructor, so functions aren't fundamentally different to any other types - at least, as far as the type system goes. Now, what about type variables? What do they do? Well now, that seems to be slightly interesting, since a type variable holds an entire type (whereas normal program variables just hold a single value), and each occurrance of the same variable is statically guaranteed to hold the same thing at all times. It's sort of like how every instance of a normal program variable holds the same value, except that you don't explicitly say what that value is; the compiler infers it. So what about classes? Well, restricting ourselves to single- parameter classes, it seems to me that a class is like a *set of types*. Now, interestingly, an enumeration type is a set of values where you explicitly list all possible values. But once defined, it is impossible to add new values to the set. You could say this is a closed set. A type, on the other hand, is an open set of types; you can add new types at any time. I honestly can't think of a useful intuition for MPTCs right now. Now what happens if you add associated types? For example, the canonical class Container c where type Element c :: * We already have type constructor functions such as Maybe with takes a type and constructs a new type. But here we seem to have a general function, Element, which takes some type and returns a new, arbitrary, type. And we define it by a series of equations: instance Container [x] where Element [x] = x instance Container ByteString where Element ByteString = Word8 instance (Ord x) = Container (Set x) where Element (Set x) = x instance Container IntSet where Element IntSet = Int ... Further, the inputs to this function are statically guaranteed to be types from the set (class) Container. So it's /almost/ like a regular value-level function, just with weird definition syntax. Where *the hell* do GADTs fit in here? Well, they're usually used with phantom types, so I guess we need to figure out where phantom types fit in. To the type checker, Foo Int and Foo Bool are two totally seperate types. In the phantom type case, the set of possible values for both types are actually identical. So really we just have two names for the same set. The same thing goes for a type alias (the type keyword). It's not quite the same as a newtype, since then the value expressions do actually change. So it seems that a GADT is an ADT where the elements of the set are assigned to sets of different names, or the elements are partitioned into disjoint sets with different names. Hmm, interesting. At the same type, values have types, and types have kinds. As best as I can tell, kinds exist only to distinguish between /types/ and / type
Re: [Haskell-cafe] Musings on type systems
On 10-11-19 04:39 PM, Matthew Steele wrote: TAPL is also a great book for getting up to speed on type theory: http://www.cis.upenn.edu/~bcpierce/tapl/ I am no type theorist, and I nonetheless found it very approachable. TAPL is surprisingly easy-going. It is long (many pages and many chapters, each chapter short), but it is the good kind of long: long but gradual ramp to get you to the hard stuff. Its first chapter explains convincingly why you should care about types to begin with (summary: a lightweight formal method). But it is not entirely for Haskell. It covers subtyping, and it doesn't cover type classes. It is also too bulky to be mobile (because it's long). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
On 19 November 2010 22:14, Albert Y. C. Lai tre...@vex.net wrote: On 10-11-19 04:39 PM, Matthew Steele wrote: TAPL is also a great book for getting up to speed on type theory: http://www.cis.upenn.edu/~bcpierce/tapl/ I am no type theorist, and I nonetheless found it very approachable. TAPL is surprisingly easy-going. It is long (many pages and many chapters, each chapter short), but it is the good kind of long: long but gradual ramp to get you to the hard stuff. Its first chapter explains convincingly why you should care about types to begin with (summary: a lightweight formal method). But it is not entirely for Haskell. It covers subtyping, and it doesn't cover type classes. It is also too bulky to be mobile (because it's long). IIRC It Does not deal Hindley-Milner type system at all. i.e. it does not cover ML's type system. Its successor ATTAPL :- http://www.cis.upenn.edu/~bcpierce/attapl/index.html Handles an ML like type systems using constraints. AFAICT This area area of type theory's history is not covered properly in any of the sources I have came across. Aaron ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
On Nov 19, 2010, at 6:22 PM, Aaron Gray wrote: IIRC It Does not deal Hindley-Milner type system at all. i.e. it does not cover ML's type system. Its successor ATTAPL :- http://www.cis.upenn.edu/~bcpierce/attapl/index.html Handles an ML like type systems using constraints. TAPL certainly covers the basic ML system -- which is pretty much the typed lambda calculus with first order polymorphism. What it doesn't do is cover type inference (or reconstruction) in any depth, although it does actually sketch at least one algorithm for HM type inference (including constraints) -- see chapter 22. You're right that ATTAPL covers much more in the realm of type inference, as well as plenty else. Cheers, Sterl.___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
On 11/19/10 4:05 PM, Andrew Coppin wrote: So what would happen if some crazy person decided to make the kind system more like the type system? Or make the type system more like the value system? Do we end up with another layer to our cake? Is it possible to generalise it to an infinite number of layers? In addition to the Coq and Agda notion of universes you should also look at Tim Sheard's Omega[1], which takes Haskell and then goes all the way up. [1] http://web.cecs.pdx.edu/~sheard/papers/SumSchNotes.ps -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
On Fri, Nov 19, 2010 at 1:05 PM, Andrew Coppin andrewcop...@btinternet.com wrote: So is Either what is meant by a sum type? Similarly, (X, Y) [...] is this a product type? Yes, and yes, although more generally speaking data Test = A Int Bool | B Test | C [Test] is a recursive ADT composed of sums (A ...| B... | C...) and products ((Int, Bool), Test, [Test]) Notionally (-) is just another type constructor, so functions aren't fundamentally different to any other types - at least, as far as the type system goes. Sort of, but I think your discussion later gets into exactly why it *is* fundamentally different. Where *the hell* do GADTs fit in here? Well, they're usually used with phantom types, so I guess we need to figure out where phantom types fit in. Well, I find it's better to think of GADTs as types that have extra elements holding proofs about their contents which you can unpack. For example: data Expr a where Prim :: a - Expr a Lam :: (Expr x - Expr y) - Expr (x - y) App :: Expr (x - a) - Expr x - Expr a (The type variables are arbitrary; I chose these specific odd ones for a reason which will shortly become clear) This can be reconstructed as an ADT with existentials and constraints: data Expr a = Prim a | forall x y. (a ~ (x - y)) = Lam (Expr x - Expr y) | forall x. App (Expr x - a) (Expr x) Conceptually, here is what these types look like in memory; [x] is a box in memory holding a pointer to an object of type x Expr a = tag_Prim, [a] or tag_Lam, type x, type y, proof that a = (x - y), [Expr x - Expr y] or tag_App, type x, [Expr x - a], [Expr x] Now, because we have type safety the compiler can actually erase all the types and equality proofs (although in the case of typeclass constraints it keeps the typeclass dictionary pointer around so that it can be used to call functions in the class). To the type checker, Foo Int and Foo Bool are two totally seperate types. In the phantom type case, the set of possible values for both types are actually identical. So really we just have two names for the same set. The same thing goes for a type alias (the type keyword). Not exactly; in the phantom type case, the two sets ARE disjoint in a way; there are no objects that are both Foo Int and Foo Bool (although there may be objects of type forall a. Foo a -- more on that later). Whereas the type keyword really creates two names for the same set. So what would happen if some crazy person decided to make the kind system more like the type system? Or make the type system more like the value system? Do we end up with another layer to our cake? Is it possible to generalise it to an infinite number of layers? Or to a circular hierachy? Is any of this /useful/ in any way? Absolutely! In fact, dependent type systems do exactly this; values can be members of types and vice versa. For example, in a dependently typed language, you can write something like data Vector :: * - Int - * where Nil :: forall a::*. Vector a 0 Cons :: forall a::*, n::Int. a - Vector a n - Vector a (n+1) append :: forall a::*, m::Int, n::Int. Vector a m - Vector a n - Vector a (m+n) append a 0 n Nil v = v append a m n (Cons a as) v = Cons a (append as v) However, - is special here, because it works at both the type level and the value level! That is, (Vector Int :: Int - *) can be applied to the value 5 to create (Vector Int 5), the set of vectors with 5 elements of type Int. And in fact, - is just a generalization of 'forall' that can't refer to the object on it's right hand side: append :: ( forall a :: *. forall m :: Int. forall n :: Int. forall v1 :: Vector a m. forall v2 :: Vector a n. Vector a (m+n) ) Since we don't refer to v1 or v2, we can abbreviate the 'forall' with -: append :: ( forall a :: *. forall m :: Int. forall n :: Int. Vector a m - Vector a n - Vector a (m+n) ) Now, however, you can run arbitrary code at the type level; just create an object with the type Vector Int (fib 5) and the compiler needs to calculate (fib 5) to make sure the length is correct! In compiler circles it's generally considered a bad thing when the compiler doesn't terminate, (one reason: how do I know if the bug is in my code or the compiler?) so these languages tend to force your code (or at least the code that can run at the type level) to terminate. There's another benefit to this: if it's possible that a type-level expression might not terminate, you lose type erasure and have to do the calculation at runtime. Otherwise you can create unsound expressions: cast :: forall a::*, b::*. (a = b) - a - b cast a b p x = x -- note that p is never evaluated, we just require the proof in scope! bottom :: forall a. a bottom a = bottom a -- if we evaluate this, we infinite loop unsound :: forall a::*, b::*. a - b unsound a b x = cast a b (bottom (a=b)) x print (unsound Int String 0) -- BOOM! Headshot to your type-safety. So, these languages
Re: [Haskell-cafe] Musings on type systems
On 11/19/10 10:05 PM, Ryan Ingram wrote: On Fri, Nov 19, 2010 at 1:05 PM, Andrew Coppin wrote: So is Either what is meant by a sum type? Similarly, (X, Y) [...] is this a product type? Yes and no. Unfortunately there's some discrepancy in the terminology depending on who you ask. In the functional programming world, yes: sum types are when you have a choice of data constructors, a la Either; and product types are when you have multiple arguments in a data constructor, a la tuples.[1] However, in set theory and consequently in much of the research on dependent types, (the dependent generalization of) function types are called ``(dependent) product types'' and (the dependent generalization of) tuples are called ``(dependent) sum types''. There's a convoluted story about why this supposedly makes sense, but it doesn't match functional programmer's terminology nor the category theoretic terminology which is often invoked in type theory. ObTangent: this is much like the discrepancy between what is meant by ``source'' and ``target'' for folks who come from a machine learning background vs people who come from a signal processing background. Thankfully, most of the NLP folks caught in the middle have decided to go with the sensible (ML) definitions. [1] In a lazy language like Haskell we have to be careful about how we phrase this. There are different notions of products[2] depending on how they behave with respect to strictness, and depending on which one you choose you'll change how you have to reason about the types abstractly. This shows up canonically in the difference between domain products and smash products. When Haskell was designed they decided not to have two different versions of products in the language, so the tuples in Haskell aren't either of these two well-behaved kinds of products. This has ramifications when people try to reason about which program transformations are valid without introducing too much or too little laziness. By and large Haskell's tuples and ADTs are good at doing what you mean, but they do complicate the theory. [2] The same is true for different kinds of sums, but that's less problematic to deal with. Notionally (-) is just another type constructor, so functions aren't fundamentally different to any other types - at least, as far as the type system goes. Sort of, but I think your discussion later gets into exactly why it *is* fundamentally different. There are a few different ways to think about functions/arrows, which is why things get a bit strange. In functional programming this is highlighted by the ideas of ``functions as procedures'' vs ``functions as data'' ---even though we like to ignore the differences between those two perspectives. In category theoretic terms, those ideas correlate with morphisms vs exponential objects (or coexponential objects, depending). There's a category theoretic relation between exponentials and products (i.e., tuples) which is where un/currying comes from. But this is also why the Pi- and Sigma-types of dependently typed languages cause such issues. For example, there's an isomorphism between A-(C^B) and (A*B)-C in certain categories, namely curry/uncurry. And there's also an isomorphism between A*B and B*A, namely swapping the elements of a pair. Together these mean, A-(C^B) ~= (A*B)-C ~= (B*A)-C ~= B-(C^A). In Haskell this is obviously true because we have Prelude.flip. However, if we generalize this to dependent functions and dependent pairs then it's no longer true in general, because B may require an A to be in scope in order to be well-kinded; e.g., assuming f : (a:A) - (b: B a) - C a b, then what is the type of swap f? So on the one hand arrows and products are just type constructors like any other, but on the other hand they're not. It's sort of like how zero and one are natural numbers, but they're specialer than the other natural numbers (you need them in order to define the rest of Nat; they have special behavior with respect to basic operations like (+), (*),...; etc). ObTangent: When we dualize things to co-Cartesian closed categories we get the same thing, except it's between sums/coproducts and coexponentials. Where *the hell* do GADTs fit in here? Well, they're usually used with phantom types, so I guess we need to figure out where phantom types fit in. Well, I find it's better to think of GADTs as types that have extra elements holding proofs about their contents which you can unpack. Ultimately, GADTs are just a restricted form of Pi- and Sigma-types. The type argument whose value varies depending on the constructor isn't actually a phantom type. You can think of there being four sorts of type variables. There are the variables for parametric polymorphism where the _same_ variable occurs on both sides of the = defining the type. There are phantom types where the variable only occurs on the left. There are existential types where
Re: [Haskell-cafe] Musings on type systems
On 11/19/10 10:05 PM, Ryan Ingram wrote: Not exactly; in the phantom type case, the two sets ARE disjoint in a way; there are no objects that are both Foo Int and Foo Bool (although there may be objects of type forall a. Foo a -- more on that later). Whereas the type keyword really creates two names for the same set. Only in a way. I'd say there certainly are values that inhabit multiple types. I'll write one right now: []. Oh, here's another: Nothing. Or even: return. Sure, these values are typically the same ones as the ones inhabiting universal types, but there's nothing terribly strange about values inhabiting multiple types. If we were strictly adhering to System F then we would have to explicitly distinguish between Nothing, Nothing @Int, and Nothing @Bool so we wouldn't have the same term belonging to multiple types. But *we don't* strictly adhere to System F, and generally speaking we like to pretend we're in Curry-style languages even when the implementation is Church-style behind the scenes. There are some nice metatheoretical benefits to using Church-style formalisms, but that doesn't mean Church was any more right than Curry. If Church were really right then we wouldn't care so much about doing type inference or about making it require as few annotations as possible, since the right thing would be to annotate the terms in the first place. It's mostly a philosophical issue (albeit with tangible metatheoretical ramifications), but there's value in both perspectives. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
