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? -- 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
