> 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? 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. 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 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. To be honest, I am not quite sure whether I like such implicit definitions. 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. Ralf ------------------------------------------------------------------------- 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
