Generic

From Esolang
Jump to navigation Jump to search

Generic is a WIP language made by User:Tailcalled in a way that makes many concepts from Category Theory easy to define.


Concepts

The main elements in the language are currently concepts. They are a way to define something in an extremely abstract way. They are a bit like interfaces or typeclasses, and are used in some of the same areas as typeclasses, but are more first-class.

Defining the concept 'Category' from category theory is done this way:

 concept Category
   obj in coll
   hom(A in obj, B in obj) in coll
   id(A in obj) in hom(A, A)
   compose(A in obj, B in obj, C in obj, f in hom(A, B), g in hom(B, C)) in hom(A, C)

'coll' is the collection of most (possibly all?) collections. Explaining each line:

 concept Category

This basically names the concept. The compiler/interpreter has to make a global collection called 'Category'.

   obj in coll

This line states that every category has a collection called 'obj'.

   hom(A in obj, B in obj) in coll

This means that there is a set for every two elements in obj. That collection is referred to as hom(A, B).

   id(A in obj) in hom(A, A)

This states that there is an element in hom(A, A) for element A in obj.

   compose(A in obj, B in obj, C in obj, f in hom(A, B), g in hom(B, C)) in hom(A, C)

This states that for every three elements A, B, C in obj, and every element in hom(A, B) and every element in hom(B, C), there is an element in hom(A, C).

One example of how concepts are more first-class than typeclasses can be seen in this definition of functors:

 concept Functor
   src in Category
   dst in Category
   F(A in src.obj) in dst.obj
   f(A in src.obj, B in src.obj, m in src.hom(A, B)) in dst.hom(F(A), F(B))

This functor has two categories, src and dst, defined like this:

   src in Category
   dst in Category

Category is the collection of all categories. Accessing a part of a specific implementation of a concept can also be done:

   F(A in src.obj) in dst.obj

This maps every element of obj in the category src to an element of obj in dst.

Actual Code

Tailcalled has currently not designed any kind of way to actually code something, but he's working on it.

Collections

Tailcalled has not yet decided on whether to use set theory, type theory or something completely different, which is why he used the word 'collection' instead of set or type. Collections might be declared with a syntax like this:

 coll List given (A in coll)
   with () -- () is the empty product
   given
     head in A
     tail in List(A)
   be
     with (head, tail)

This makes anything of the form (a, (b, (c, (d, (e, (f, ())))))) a list iff a-f are all in one collection. A collection of disjoint unions could be defined like this:

 coll Sum given (A in coll, B in coll)
   given
     fst in A
   be
     with (#false, fst)
   given
     snd in B
   be
     with (#true, snd)

This system would probably require something that's equivalent to dependent typing.