Ralf Hemmecke <[EMAIL PROTECTED]> writes:
| > What is nonconstructive about
| > forall(T: Type)
| > identity(T x) == x
| > which can be used as
| > identity 4.4 -- T deduced to Float
| > identity "string" -- T deduced to String
| > ?
|
| Just one remark it certainly is a bit off-topic.
|
| You certainly know that Aldor has functions of the form
|
| string: Literal -> %
|
| that can be exported and implemented by any domain.
| Do you intend to provide something like that in OpenAxiomm, too?
I saw the suggestion, I've yet to convince myself that it solves the
original problem it was intended to solve conveniently. Certainly
that is not the only design choice. For example, the domain Literal
could have been parameterized by the type of the fundamental domain of
the literal, so that I could write
coerce: Literal String -> %
instead of `moving the type of the literal into the function name'.
Haskell also uses a different design choice. The design space is not
a singleton. I have to appreciate better the problem to pick one of
the solutions. I know where I would like to see literal 4
interpreted in a way I want; that isn't my problem with the proposed
Literal domain.
|
| So then if I add a function
|
| string(l: Literal): % == 1;
|
| to the definition of Float, the statement
|
| identity "string"
|
| becomes ambiguous. I don't think that is a problem.
Now, we have double ifs. But just in case OpenAxiom has the domain
Literal (not parameterized), I don't see the ambiguity: T is deduced
to Literal. If it had the parameterized form, again I don't see the
ambiguity: T is deduced to Literal String.
|
| But still, I think the forall above is fine.
| In fact, it can already be used today since "forall" can be seen as a
| parametrized package that exports a function
|
| identity: T -> T
Today, Spad uses a form of System F style programming: type
parameters are Lambda-bound, and one usually bind them as
(category or domain) constructor arguments. Next, one relies on the
interpreter to do type inference to somehow figure out the value for
T. This works to some extent in the interpreter, but fails miserably
in the library -- at least the programming style becomes unbearable.
This is exactly the discussion we had at the workshop in Hagenberg.
Universal quantification is trivially translated to System F -- in
fact Haskell's core semantics is System F augmented with constants --
by translating universal quantification to Lambda-binding.
Given this translation, I'm a bit puzzled the idea of universal
quantification is generating so much reaction...
|
| But I guess, you want to experiment with some kind of mechanism that
| removes the burden from a programmer of defining such a "forall"
| explicitly.
No, I want the programmer to explicitly declare the forall, then have
the compiler deduce the values for the quantified parameters in call.
In System F, on writes
identity(T: Type, x: T) == x
I find the call
identity(String, "foo")
unecessarily verbose, when
identity "foo"
would suffice. For that, I want a mechanism that identifies which
type variables need to be supplied, and which are deduced.
Second, I would like to be able to define a domain such as
MyVar(): SetCategory with
coerce: forall (s: Symbol) . Variable s -> %
-- ...
== add
Rep == Symbol
forall(s: Symbol) .
coerce(x: Variable s): % == per s
-- ...
At the moment, to achieve the coerce above, I need to introduce
another package that would be parameterized by 's' and will do the
coercion. But for that coercion to be possible, I need a function
that somehow reveals (in some sense) the representation of MyVar so
that I can call it to coerce a Variable s to MyVar. That way of doing
thing unnaturally (to my view) breaks domain implementation into
packages only to work around a limitation the purpose of which I do
not understand.
I would like to write codes at their abstract level, and reflect my
thinkings as opposed to writing in terms of bit-level instructions.
We don't need to force the System F style programming -- even when use
System F as underlying model.
| To be honest, I am not quite sure whether I like such implicit
| definitions.
I believe I never proposed implicit definitions. If there is one,
then I must have missed it.
| What I know about Haskell so far, they then have this
| concept of specifying the type or T with some => thing... sorry I
| don't remember the details, but to me it looked exactly like
| definition of a parametrized domain in Aldor.
|
| Could you give some words about where you are aiming at? Thanks.
See above. A posterchild example is the identity function above.
And, I would like to know exactly what people are `complaining' about,
and why they are `unhappy' with the idea of universal quantification
parameters. Preferably something other than `strange' or `heavy
weight' :-)
-- Gaby
-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
