Bill Page <bill.p...@newsynthesis.org> writes: | 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.
Indeed, if you have a contructor in application position, the interpreter and the compiler should give same result -- modulo "bugs". Otherwise, the compiler will be confused and only the interpreter will do something sensible. This is because the interpreter has a latitude of using the naive approach of reducing type expressions to values and carry on computation. The compiler does not necessarily have that luxury in general. -- Gaby ------------------------------------------------------------------------------ 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
