Bill Page <bill.p...@newsynthesis.org> 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 ------------------------------------------------------------------------------ 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
