On Wed, Aug 6, 2008 at 10:07 AM, Gabriel Dos Reis wrote:
>
> | > 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
> | > ?
> ...
> Ralf Hemmecke writes:
> |
> | 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
>
As a specific example of such a package lets consider:
MyId(T:Type): with
identity: T -> T
== add
identity(x:T) == x
If 'MyId' is exposed in the interpreter then
identity(2.2)
could be instantiated by function selection as
identity(2.2)$MyId(Float)
> 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.
>
Could you give an example from the Axiom library where this "fails
miserably"? In what way is the resulting style "unbearable"?
Or is it just this is rather awkward because function selection (type
inference) in the compiler is significantly less powerful than in the
interpreter?
> 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...
>
The odd thing for me here is that I would not like to call this
"universal quantification" but rather existential quantitification.
When I write:
identity(x: T) == x
in the package definition above, I mean (implicitly) that there exists
some type T for the value that I will provide for x. The package and
function selection mechanisms just finds such a T. Perhaps I am just
confused about the terminology.
>
> |
> | 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, one 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.
>
In principle all free type variables should be deduced, no?
> 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
> -- ...
Did you mean?
coerce(x: Variable s): % == per Symbol
>
> 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.
>
Thank you. I think that is an excellent example but I do not
understand why you say that you "need to introduce another package".
Why not just write:
MyVar(s:Symbol): SetCategory with
coerce: Variable s -> %
-- ...
== add
Rep == Symbol
coerce(x: Variable s): % == per Symbol
-- ...
and let the interpreter make the usual type inference? Do you think it
is "unnatural" to implicitly use MyVar with such a free parameter?
> ...
> 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' :-)
>
In this context, as Ralf said, it does not seem to be anything extra
that is not already done by Axiom. Perhaps I am missing something.
Regards,
Bill Page.
-------------------------------------------------------------------------
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
