Let me take a shot at this.
Jan Brosius writes:
> Now I have some difficulty to follow. If I write
>
> id :: a -> a
>
> then I thought it meant " id is a "function" from type a to type a " ; in
> logic this is completely equivalent with (since a is a variable ):
> " forall a ( id is a function from type a to type a) "
> But then I immediately get a problem, indeed since id is a
> function from set
> a into set a then I have
> id is a subset from set aXa (the product of a with a)
> Choose a set b such that "a intersection b = empty" then
> id is subset of aXa and subset of bXb
> which is a contradiction. So id is not a function but one can define it as
> id = \x -> x that is an untypable lambda-function.
First, typeability (sp?) is not a property you can define in a vaccuum; you
have to specify typeability with respect to a set of axioms. In a
simply-typed lambda-calculus, the best you can do is to split id into a
collection of functions, one for each type. If it's a Church-style calculus,
\x.x is not even a well-formed term, since it lacks a type for its domain.
If it's Curry-style, I think you need to supplement the term with a type
assignment; there is no way to quantify a type in simply-typed
lambda-calculus, but you can still give it a type A -> A, for any A you
choose.
In SOLC (second-order lambda-calculus), you would not define it as simply
\x. x, but rather
/\X.\x.x, which can be assigned the type Pi(X).X->X, so it is certainly
typeable in that system.
> A way out of it is to write id(a) :: a -> a ; then I can really say that
> forall a ( id(a) is a function from type (or set) a into (or to) type a).
Yes, that is how you express it in SOLC: id = /\X.\x.x : Forall X. X -> X.
> And forall x forall a (id(a) x = x) which is completely equivalent with
> forall x forall a (id(a) x = x).
Be careful; you are quantifying over two different domains here. a is a
collection of x's. If you include them in the same domain, then I think you
run into size problems.
> I am very confident that you cannot go around the rule:
> forall a forall b ( T(a,b)) equivalent with forall b forall a
(T(a,b)).
>
> So I think, before I can proceed any further in learning I invite you to
> phrase exactly what one means with
> id :: a -> a ?
It means that id cannot observe (read: destructure) its argument.
The way I know to model this is in category theory: if h : forall A. A -> A,
then h is a natural isomophism from and to the identity functor I:C=>C on
the category C modelling your calculus. (BTW, category theory completely
separates the domains of terms and types, so it is easier to avoid size
problems.) In this case, saying that h is a natural isomorphism means that
for each term f:A->B, \a.f (h A a) = \a.h B (f a). This seems natural enough
(excuse the pun) if h = id, but what is really striking about it is that
this holds for _any_ definition of h, i.e., it is a property that can be
inferred solely from the typing. For example, we know just from the fact
that concat : Forall a. a -> a, that
\xs.map A B f (concat A xs) = \xs. concat B (map A B f xs)
where map : forall a. forall b. A -> B -> ([A] -> [B]). Here the endofunctor
in question is the list functor, []. This idea is often called "theorems for
free", since they are independent of the definition; things like the
equation above can be significant language optimizations.
In fact, id : forall A. A -> A means a little more than naturality: id has
to have the same implementation at each type A, which is not true in general
of all things that can be denoted by a natural transformation. But in
"vanilla" SOLC, I think, all the terms that denote natural transformations
obey this property. In Haskell, though, you could write:
class Id a where
id :: a -> a
instance Id Int where
id x = x + 0
etc., so that the instance at each type uses a different algorithm. For the
identity function, no one would do this of course because it is clearly
_parametrically_ polymorphic. Anyway, the type for this id is not quantified
the same way as it is for the parametric version, because the implementation
can depend on the particular type. You can't do this in SOLC, since to use
/\-abstraction, the type variable A in /\A.x must not appear in the
environment of x. That's why you can't write /\A.x if x:A.
(I wrote vanilla SOLC above, because I don't know if this is true for some
extensions of SOLC, in particular extensions with subtyping or bounded
quantification, but also the more general calculus where you can quantify
over type constructors. Maybe someone else knows?)
> > > I have already read all available online documentation.
> > > In logic one has: forall x forall y = forall y forall x.
> >
> > This is not the case in the second-order lambda calculus, because the
> > order of the type lambdas is clearly significant:
> >
> > (.) :: \/a. \/b. \/c. (a->b) -> (b->c) -> (a->c)
> >
> > is clearly different from
> >
> > (.') :: \/c \/b. \/a. (a->b) -> (b->c) -> (a->c)
> >
> > although the two are in some sense equivalent.
> >
> >
> What do you mean by " in some sense equivalent and yet clearly
> different" ?
He means that they are interderivable. Given (.), you can define (.') and
vice versa, for example:
(.) = /\ A. /\ B. /\ C. (.') C B A
--FC
