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
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
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]
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
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
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):
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
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
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
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:
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
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.
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
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
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
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
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
17 matches
Mail list logo
