Bill Page <[email protected]> writes: | And just so I don't give the wrong impression I should not fail to | point out that this sort of dependent type does also work in SPAD: | | (1) -> )sys cat dep1.spad | | )abbrev domain F f | f(x:Ring) : LinearAggregate(x) == List (x)
this the easy case and has been working in Spad as long as I have known Spad for that is the way domain constructors work :-) 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. -- 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.
