Thanks for the thorough response.
I've found BarrasBernardo's work (at least, slides) about ICC*, I'll
have a look at it.
Could you provide with names of works by Altenkirch/Morris/Oury/you?
The unordered pair example was especially interesting, since I am
somewhat concerned with which operations
Thanks, at least the title looks like exactly what I've been looking
for, however I cannot quickly appreciate the notation-heavy contents:
I definitely will as soon as possible.
2009/5/20 Masahiro Sakai masahiro.sa...@gmail.com:
From: Eugene Kirpichov ekirpic...@gmail.com
Date: Sun, 17 May 2009
Hi
On 20 May 2009, at 07:08, Eugene Kirpichov wrote:
Thanks for the thorough response.
I've found BarrasBernardo's work (at least, slides) about ICC*, I'll
have a look at it.
Could you provide with names of works by Altenkirch/Morris/Oury/you?
The unordered pair example was especially
Or in a language without bottoms.
2009/5/20 David Menendez d...@zednenem.com:
On Sun, May 17, 2009 at 11:52 PM, Ryan Ingram ryani.s...@gmail.com wrote:
Free theorem's are theorems about functions that rely only on parametricity.
For example, consider any function f with the type
forall a.
On Sun, May 17, 2009 at 11:52 PM, Ryan Ingram ryani.s...@gmail.com wrote:
Free theorem's are theorems about functions that rely only on parametricity.
For example, consider any function f with the type
forall a. a - a
From its type, I can tell you directly that this theorem holds:
forall
From: Eugene Kirpichov ekirpic...@gmail.com
Date: Sun, 17 May 2009 23:10:12 +0400
Is there any research on applying free theorems / parametricity to
type systems more complex than System F; namely, Fomega, or calculus
of constructions and alike?
You may be interested in this:
The Theory of
Hi
Questions of parametricity in dependent types are made more
complex by the way in which the Pi-type
(x : S) - T
corresponds to universal quantification. It's good to think
of this type as a very large product, tupling up individual
T's for each possible x you can distinguish by
Hello,
Is there any research on applying free theorems / parametricity to
type systems more complex than System F; namely, Fomega, or calculus
of constructions and alike?
This seems very promising to me for the following reason: Take the
free theorem for 'sort::(a-a-Bool)-[a]-[a]'. The theorem
On Sun, 17 May 2009 23:10:12 +0400
Eugene Kirpichov ekirpic...@gmail.com wrote:
Is there any research on applying free theorems / parametricity to
type systems more complex than System F; namely, Fomega, or calculus
of constructions and alike?
Yes. I did some research into it as part of my
I'm glad that someone is doing research in that direction!
Are your results so far applicable to create a free theorem for that
example with sortBy?
2009/5/17 Robin Green gree...@greenrd.org:
On Sun, 17 May 2009 23:10:12 +0400
Eugene Kirpichov ekirpic...@gmail.com wrote:
Is there any research
This word has piqued my interest, I've hear it tossed around the
community quite a bit, but never fully understood what it meant. What
exactly is a 'free theorem'?
Eugene Kirpichov wrote:
Hello,
Is there any research on applying free theorems / parametricity to
type systems more complex than
Free theorem's are theorems about functions that rely only on parametricity.
For example, consider any function f with the type
forall a. a - a
From its type, I can tell you directly that this theorem holds:
forall g :: A - B, x :: A,
f (g x) = g (f x)
(Note that the f on the left
12 matches
Mail list logo
