Bill Page <[email protected]> writes: | On Fri, Aug 19, 2011 at 4:03 PM, Gabriel Dos Reis <[email protected]> wrote: | > Bill Page <[email protected]> writes: | > | > | On Fri, Aug 19, 2011 at 3:34 PM, Gabriel Dos Reis <[email protected]> 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 <[email protected]> | 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 <[email protected]> | | | 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 -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.
