Am Freitag, 24. Februar 2006 17:29 schrieb Conor McBride: > [...] > If I were defining this structure I might try something like this (which > is suspiciously vector-like): > > ------------------------------------------------- > ( H : Nat -> * ! > ! ! > ! n : Nat > data !--------------! > ! Tm H n : * ) > > ( f : Tm H (suc n) ! > ! ! > ( h : H n ! ! a : Tm H zero ! > where !-----------------! ; !------------------! > ! head h : Tm H n ) ! app f a : Tm H n ) > ------------------------------------------------- > > You can get your terms by appropriate choice of H and n. Of course, I've > buried the head symbol inside, so that could cause trouble in other > ways.
Oh, I fear I really don't understand the idea behind this code. :-( > [...] > Back at base, we're looking to exploit the theory of containers to > characterise a much more liberal notion of strict positivity, with > coinductive types, mutual definitions etc. Roughly, you'll be able to > define (Vec n X) in such a way that it is explicitly a container for X: > this carries the requirement that Vec's constructors be strictly > positive in X as well as in Vec, which they are, but it yields the > reward that you can use Vec as a strictly positive operator in > constructing other types. As a bonus, you'll also get all sorts of > functoriality gadgets for free. This sounds good. ;-) > [...] > This is just one design space in which there's plenty of scope for > constructive contributions. The Awkward Squad, anyone? While we are at contributions: In which way could a beginning postgraduate who is very much interested in Epigram contribute to it? I'm currently employed as a teaching assistant at the Brandenburg University of Technology at Cottbus, Germany and want/need to create a PhD thesis. My professor gave me certain freedom in choosing the topic of my thesis. So I asked him if something about Epigram would be in his interest and he told me that he is principally open for such a topic. > Cheers > > Conor Best wishes, Wolfgang
