On Wed, Aug 6, 2008 at 11:22 AM, Bill Page <[EMAIL PROTECTED]> wrote: > On Wed, Aug 6, 2008 at 11:36 AM, Gabriel Dos Reis wrote: >> "Bill Page" <[EMAIL PROTECTED]> writes: >> >> (1) So you consider >> >> MyId(T:Type): with >> identity: T -> T >> == add >> identity(x:T) == x >> >> much less `heavy weight' than a simple free function >> >> forall(T: Type) >> identity(T x) == x > > identity(x:T) == x > >> >> ? >> > > No, now that I think I am beginning to understand what you mean it > seems to me that they are essentially identical.
I believe I expressed that in a previous message: # 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. # [...] # 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... -- 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
