<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><blockquote type="cite"><div>I think the problem is not about positive functors not having a fixed point but about strictly positive functors not recognized by the Agda positivity checker.<font class="Apple-style-span" color="#000000"><font class="Apple-style-span" color="#144FAE"><br></font></font></div></blockquote><div><br></div>I was just remarking that we can express the type of strictly positive functors as containers.<br><div><br></div><blockquote type="cite"><div>About you complaint on how many function types we might get...<br><br>I think a language is well-designed if it has all the abstractions. Or stated differently, the user should be able to roll his own constructs which are analogous to those he finds in the system. Otherwise there will be always frustrating limits, like:</div></blockquote><blockquote type="cite"><div><br>* The language has built-in infix operators but I cannot define my own.<br> Solved by Haskell.<br><br>* The language has its own special forms (like short-cut binary ops) but<br> I cannot define my own because of call-by-value.<br> Solved by Haskell's call-by-need.<br><br>* I can define my own special forms but not give them a nice syntax like<br> if_then_else_<br> Solved by Agda's mixfix operators.<br><br>* I can define strictly positive functors but not abstract over them.<br> Solved by MiniAgda's polarities.<br><br>* I can build data structures but not abstract over them.<br> Solved by ML's functors.<br> Solved somewhat by Haskell's type classes.<br> Solved somewhat by Agda's records<br> (what is missing here are abstract reductions).<br><br>We've come far, but not far enough.<br></div></blockquote><div><br></div><div>I understand what you mean but I think there are too many potentially desirable refinements of function types to result in a type theory which is still comprensible or usable. Another interesting option is coercion space corresponding to coercive subtyping, or your parametric function space, not to forget the injective function space and obviously the annotations one needs for type-based termination. </div><div><br></div><div>I am not sure the monster we will end up could be called "well designed".</div><div><br></div><div>Type Theory is rich enough to express these conditions semantically. What we need is an easy way to combine the convenient syntax we want to use with the semantic conditions they refer to. The soundness proof is then replaced by the elaboration of the syntax.</div><div><br></div>Cheers,</div><div>Thorsten<br><blockquote type="cite"><div><br>Cheers,<br>Andreas<br><br>On 11/19/10 11:05 AM, Thorsten Altenkirch wrote:<br><blockquote type="cite">You cannot in general construct fixpoints of arbitrary functors, e.g. FX = (X->2)->2 hasn't got an initial algebra in Type Theory.<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">If you want to have fixpoints you should refer to containers, i.e. S : Set, P : S -> Set which give rise to the functor FX = Sigma S (\ s -> Ps -> X). The initial algebra of a container is given by the W-type W S P.<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">Cheers,<br></blockquote><blockquote type="cite">Thorsten<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">On 19 Nov 2010, at 08:33, Dominique Devriese wrote:<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite"><blockquote type="cite">Thorsten,<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">2010/11/18 Thorsten Altenkirch<<a href="mailto:txa@cs.nott.ac.uk">txa@cs.nott.ac.uk</a>>:<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">I just wonder how many different functions spaces we'll end up with.<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite">If one wants to quantify over functors why don't you just do that? I mean define Functor : Set1 as a record (extending RawFunctor from the library) and then show that it is closed under various operations?<br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">I think I understand what you mean, but wouldn't this ultimately<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">require some form of collaboration from the positivity checker when<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">taking a data type fixpoint as in my EventHandlerMonad example above?<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Dominique<br></blockquote></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite"><br></blockquote></div></blockquote></div><br></body></html>