Re: [open-axiom-devel] What can be done with types as first-class objects?
A system for computer algebra and symbolic mathematics
Brought to you by:
dos-reis
From: Gabriel D. R. <gd...@cs...> - 2011-08-19 20:03:17
|
Bill Page <bil...@ne...> writes: | On Fri, Aug 19, 2011 at 3:34 PM, Gabriel Dos Reis <gd...@cs...> 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 |