I find myself wanting a way to define types inductively like this: X := Union(A,T X)
so X is an infinite sequence of types: A /\ T A /\ T T A /\ ... where: A:Type -- base type T:X -> X -- endofunctor but this is a circular definition, in order to break this circle perhaps we could start by defining T as T: Type->Type and then constraining it to T:X -> X in concrete implementations. Can anyone suggest a variation of the following that would be valid in SPAD: MonadCat(A:Type,T: Type->Type) : Category == with X ==> Union(A,T X) unit :X -> T X mult :T ( T X) -> T X So if we take a concrete instance of List then: X := Union(A,List A,List List A, List List List A ...) I get the impression that there is a hack in the List implementation that allows this? That is, when checking list types, the compiler does not look too deeply into the nested types? Perhaps if lists were implemented as monads such hacks would not be needed? The above is done purely in terms of types/categories which would be the ideal way to implement monads but perhaps there is a less powerful but more easily implemented way to implement monads in terms of domains. In this case representations can be implemented inductively (co-data types), in category theory terms perhaps this is like working in terms of components? So List is a monad with mult and unit defined as follows: List(S: Type) is a domain constructor Abbreviation for List is LIST This constructor is exposed in this frame. ------------------------------- Operations -------------------------------- .... concat : List(%) -> % -- mult list : S -> % -- unit .... Martin -- 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.
