On Fri, Aug 19, 2011 at 4:03 PM, Gabriel Dos Reis <g...@cs.tamu.edu> wrote: > Bill Page <bill.p...@newsynthesis.org> writes: > > | On Fri, Aug 19, 2011 at 3:34 PM, Gabriel Dos Reis <g...@cs.tamu.edu> wrote: > | > > | > I thought you were after something more elaborate where an operation > | > from a domain has a dependent type... > | > > | > Note also that Spad does not work properly with operations returning > | > types -- for very deep implementation reasons, one that the Haskell > | > people also faced when they added type families (i.e. type-level > | > functions, still not accepting values at that level) leading to redesign > | > of Haskell type rules and extension of its theoretical foundation. > | > > | > | Here is a domain exporting an operation that returns a type. Although > | one might claim that the type that it returns is not explicitly > | dependent ... > > I am not sure I understand the conclusion you wanted to draw from the > example. I thought I explicitly mentioned type families, which by definition > involve application of a non-contructor in operation position. Again, I > might have missed the conclusion you wanted to draw. Could you state > it in an unambiguous form? >
These examples were in response to Yrogirg's question: ---------- Forwarded message ---------- From: Yrogirg <yrog...@gmail.com> Date: Fri, Aug 19, 2011 at 10:16 AM Subject: [fricas-devel] Re: What can be done with types as first-class objects? To: FriCAS - computer algebra system <fricas-de...@googlegroups.com> And can a function return something like (x : Ring) as a result with dependent types? For example f : Type == List (x : Ring) ---- I was trying to interpret what he might have meant by this question. My only conclusion so far is that there are several possible interpretations. My observation (which what was perhaps what triggered you interest) was that the interpreter seems to use a different interpretation than the compiler. Regards, Bill Page. ------------------------------------------------------------------------------ Get a FREE DOWNLOAD! and learn more about uberSVN rich system, user administration capabilities and model configuration. Take the hassle out of deploying and managing Subversion and the tools developers use with it. http://p.sf.net/sfu/wandisco-d2d-2 _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
