Talk:Generic

For what it's worth, the category example can be translated basically verbatim to Coq or Agda (except instead of sets it's types). There's an (IIRC, well-known) paper that basically starts like that and goes on to define a fair bit of category theory in Coq. —ehird 17:51, 8 January 2012 (UTC)

Cool, but there are several problems with Coq/Agda. They are total, I think they are unreadable, if it's types instead of sets it won't be generic enough. I'll eventually make Generic Turing-complete (the compiler will probably be Turing-complete too), FYI. --Tailcalled 19:00, 8 January 2012 (UTC)

They are total

This is required, or they would be logically inconsistent (and so all your proofs would be worthless).

I think they are unreadable

Fair enough. Agda's Unicode is daunting; Coq's syntax is regular, but the tactic proofs are pretty ugly.

if it's types instead of sets it won't be generic enough.

Err? Type theory is as sound a foundation for mathematics as set theory; types just as generic as sets. I was just pointing out an interesting tidbit, anyway, not suggesting you use one of those instead of making your own language :) —ehird 19:21, 8 January 2012 (UTC)

This is required, or they would be logically inconsistent (and so all your proofs would be worthless).

Yeah, but I'm not making a proof system :)

Err? Type theory is as sound a foundation for mathematics as set theory; types just as generic as sets. I was just pointing out an interesting tidbit, anyway, not suggesting you use one of those instead of making your own language :)

They are? I've always heard that type theory was based on set theory, so I assumed it wasn't as powerful. In that case I'll think about basing Generic on type theory. --Tailcalled 21:09, 8 January 2012 (UTC)

I was just pointing out an interesting tidbit, anyway, not suggesting you use one of those instead of making your own language :)

Huh. I guess I'm too used to people wanting to know why I'm making something new. Or rather, people saying I'm reinventing the wheel too much. --Tailcalled 21:12, 8 January 2012 (UTC)

They are? I've always heard that type theory was based on set theory, so I assumed it wasn't as powerful. In that case I'll think about basing Generic on type theory.

Nope, type theory is a foundation itself. The main nice thing you get over set theory is that (most) type theories are computable, becoming dependently-typed lambda calculi through the Curry-Howard lens. Indeed, you can quite easily encode set theory in most type theories, although you don't get much computation out of it. —ehird 21:38, 8 January 2012 (UTC)

Huh. I guess I'm too used to people wanting to know why I'm making something new. Or rather, people saying I'm reinventing the wheel too much.

Not much of that around here* :) —ehird 21:38, 8 January 2012 (UTC) (wow, this nesting is really confusing...)

* unless you make a BF derivative

I've got an idea! I'll reinvent the wheel! Seriously though, maybe it would be best if I invented a new system for describing collections that fits Generic better. I'll look into some type theory, but if I don't find anything fit for Generic, I'll probably invent a new system. The primary reason that I haven't started on the code yet is because I need to create a way to write and use collections in a simple yet powerful way. Unfortunately I don't have a very broad knowledge about math as I'm only a hobby programmer.

One way of defining collections that I would like is having a finite 'seed' collection, which contains the values to put in the start of the collection, and a finite 'grower' collection, which contains the functions to apply to every element of the collection to get a new element. For example, the (infinite) collection of Peano numbers could be defined like this: Coll({0}, {x -> Sx}). Do you know anything which allows this? (or anything that disproves it) --Tailcalled 21:57, 8 January 2012 (UTC)

Actually, it would be an idea to define Coll so it's the <*> of an applicative functor, and {x} so it's the pure of an applicative functor. It's incredibly unlikely that I will be able to do that, but it would be nice to define products like this: Coll(x, Coll(y, {f -> s -> (f, s)})) --Tailcalled 22:06, 8 January 2012 (UTC)

I should probably say that it is unlikely that it is an applicative functor, but I can't resist trying to define Coll so it is an applicative functor. --Tailcalled 22:34, 8 January 2012 (UTC)

Yeah, it's not an applicative functor. :( --Tailcalled 22:35, 8 January 2012 (UTC)

Well, if it's total genericity you're going for, something like type theory is immeasurably more generic than such a collection interface; for instance, I don't think your Coll can even represent a single uncountable set. (I don't think it can represent most functions (with infinite domain), either (assuming the standard set theory definition of a function as a set of (input,output) pairs with some laws)). Of course, it's also more difficult to implement :) —ehird 22:39, 8 January 2012 (UTC)

Total genericity would probably not be a good idea, as it would be nice if 'typechecking' was generally solvable. I don't think there would be any reason for Coll to be able to describe uncountable collections. The biggest problem is making it possible for Coll to describe useful collections. --Tailcalled 23:01, 8 January 2012 (UTC)

Remove

Can some admin remove this page? Designing this to be generic enough will make it unrecognizable. --Tailcalled 10:33, 21 January 2012 (UTC)

I'm in favour of keeping it per the discussion Smjg mentioned, especially since it's already in Category:Ideas. —ehird 15:02, 21 January 2012 (UTC)