Re: [Haskell-cafe] ANN: data-category, restricted categories

2010-03-30 Thread Edward Kmett
Very true. I oversimplified matters by mistake. One question, I suppose, is does seq distinguish the arrows, or does it distinguish the exponential objects in the category? since you are using it as an object in order to apply seq, and does that distinction matter? I'd hazard not, but its curious

Re: [Haskell-cafe] ANN: data-category, restricted categories

2010-03-26 Thread David Menendez
On Fri, Mar 26, 2010 at 11:07 AM, Edward Kmett wrote: > > On Fri, Mar 26, 2010 at 11:04 AM, Edward Kmett wrote: >> >> -- as long as you're ignoring 'seq' >> terminateSeq :: a -> Unit >> terminateSeq a = a `seq` unit >> > > Er ignore that language about seq. a `seq` unit is either another bottom o

Re: [Haskell-cafe] ANN: data-category, restricted categories

2010-03-26 Thread Edward Kmett
On Fri, Mar 26, 2010 at 11:04 AM, Edward Kmett wrote: > > -- as long as you're ignoring 'seq' > terminateSeq :: a -> Unit > terminateSeq a = a `seq` unit > > Er ignore that language about seq. a `seq` unit is either another bottom or undefined, so there remains one canonical morphism even in the

Re: [Haskell-cafe] ANN: data-category, restricted categories

2010-03-26 Thread Edward Kmett
On Mon, Mar 22, 2010 at 12:33 PM, Sjoerd Visscher wrote: > > Of course the are still a lot of things missing, especially in the details. > And I'm a category theory beginner, so there will probably be some mistakes > in there as well. F.e. Edward Kmett doesn't like () being the terminal > object i

[Haskell-cafe] ANN: data-category, restricted categories

2010-03-22 Thread Sjoerd Visscher
Hi everybody, At ZuriHac I released data-category. It is an implementation of several category-theoretical constructions. I started this library to learn about both category theory and type level programming, so I wanted to implement the CT concepts as directly as possible. This in contrast to