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. Regards, Bill Page. -- 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.
