Am Montag, 27. Februar 2006 11:33 schrieb Conor McBride: > [...] > Wolfgang Jeltsch wrote: > [...]
> >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. > > This is a very good and timely question. There are lots of things to > think about, most of which go 'how should we treat feature X in > Epigram?', which tends to decompose into three parts 'how should feature > X appear to the programmer?', 'how do we model feature X in our type > theory (extending it if necessary)?' and 'how might the elaborator get > from one to the other?'. And possibly a fourth 'what has become easy > which was hard before?'. There's a large collection of candidates for > feature X, plenty enough to share around: polymorphic stratified > universes, coinduction, IO, the Partial monad, monads and other notions > of computation generally, induction-recursion, datatype refinement, > reflection, generic programming, program specification and derivation, > linearity, quotients, modules, I could go on and I'm sure others could > too... Oh dear, it seems that it took me almost half a year to answer this e-mail. (But this doesn't mean that I was sleeping during this time. For example, I have spent a notable amount of time reading about such nice things as category theory and type theory—besides my teaching work and a nice two-week trip to Nottingham ;-).) What interests me know is whether you or some other person could recommend me certain papers or whatever which explain the above-mentioned topics to some degree, give background information, state the state of the art, etc. For example, I currently have no clue what polymorphic stratified universes are (and the only Google hit for this phrase is the mail archive page of the e-mail I'm just replying to :-) ). > [...] > But I think I should probably stop writing here and put more of this on > a blog page where others can add to it too. There should be some sort of > space for 'open topics' with useful links and half-ideas. These things > tend to live in people's heads at the moment, brought out only on the > back of an envelope in the pub (eg, yesterday's bout of corecursive > programming down the Vic with Hank which helped things along > tremendously). I'll get that page going as soon as I can. Does there exist such a page meanwhile? > All the best > > Conor Best wishes, Wolfgang
