Croof Ideas

Here I will put down some ideas I had for croof in the past days

Croof Syntax

Set Definitions

To define a set we are going to use the `def` keyword, followed by a *capitalized* word. Then we have an equal sign and a set expression. In this first example, the set expression is delimited by `{` and `}`. But we might also want to allow things like operations between sets.

Lets first take a look at a couple set definitions:

```croof def Bool = { "false", "true" } def Bit = { 0, 1 } ```

Now, I think what is important is that inside the set expression we can have different things. In this example we have strings using `"` and numbers.

What would be kind of cool is a set being able to contain anything as long as it has the same type. For instance:

```croof def A = { "a" } def B = { "b" } def C = { "c" } def Sets = { A, B, C } ```

In this case we have a set called "Sets" that contains other sets as elements. This could allow on operations made on sets.

Functions and Operators

I was thinking that for operators/functions you need to define all the "pattern matching" behaviour in one place.

That way you can't just inject stuff like "1 + 1 = 3" in the REPL.

```croof def + : N -> N -> N where forall a : N, forall b : N => a + b = b + a ... end ```

Now, some problems I see. You can still just define a new operator and then define "1 + 1 = 3" in there. How can we make sure that these definitions are good? I guess one way could be to force that the main operation that is being done is the one that is defined. Think of this as "we define PLUS, so in the axioms we should define how PLUS works".

Let's look at other examples

```croof def * : N -> N -> N where forall a : N, forall b : N, forall c : N => a * (b + c) = a * b + a * c ... end ```

Here you can see that we define MULT (as "*") and then we have the main operator on the left hand side of the equation as MULT again. Which I think should be good enough.

Built-in

Now let's take a look at some things that we might need, but we cannot really express in this language. Let's say that we want the set of all Int numbers. Well... we cannot really do that in this language... we can try to write all the numbers by hand but that's not really feasable. This means that we need some kind of built in for infinite sets. Let's say we might want infinite sets for multiple things. One of them is obviously numbers. Maybe we want to call it "Int" or "Integers" I guess "Int" is good enough. I also think that for this language to be cool we want to allow Big numbers to exist. So we might want to not limit on int64, but to allow arbitrary sized numbers. That is fine. Let's say we add this set "Int". This will contain any number from -inf to +inf. Let's also say that we need floats, we could add a set "Real" that spans the same -inf to +inf, but also contains all float numbers. Keep in mind that these are just concepts. We cannot really write down one of these sets and expand them. We might be able to sample them, and get some kind of random value out. But we are not able to visualize the entire set. That should not be allowed.

Last set that I think would make sense to be built in is "U". This would represent the Universe set, that contains all other sets. Any set that you can think of, should be included in U. Why is this useful? Well, we might want to have operators that work on sets. For instance union, intersection etc. These operators need a type, and U can be that type. Good.

Actually maybe another set that can be nice to have is the set of all strings. But at this point IDK... like you could even say the set of all operators, or the set of all functions. But is that really needed? Since we have U that might not be needed... I mean... with U existing, do we need any other set?

Just like we define an operator we might be able to define a set similarly.

```croof def N : U where ... end ```

but now the question is what can we put in that where. We need some statements.

What if we allow recursive definitions?

```croof def N : U where def zero : N where zero = 0, end, def succ : N -> N where ... end, end ```

We all know that succ is something really specific for Natural numbers.

Revised stuff

```croof def N where 0 : N, succ : N -> N, end

def + : N -> N -> N where add_zero_left :: forall b : N => 0 + b = b, add_succ_left :: forall a : N, forall b : N => succ(a) + b = succ(a + b), end

add_zero_right :: forall a : N => a + 0 = a proof case 0 => 0 + 0 = 0 [add_zero_left], case succ(a') => succ(a') + 0 = succ(a' + 0) [add_succ_left] = succ(a') [IH], end

add_succ_right :: forall a : N, forall b : N => a + succ(b) = succ(a + b) proof case 0 => 0 + succ(b) = succ(b) [add_zero_left], succ(0 + b) = succ(b) [add_zero_left], case succ(a') => succ(a') + succ(b) = succ(a' + succ(b)) [add_succ_left] = succ(succ(a' + b)) [IH], succ(succ(a') + b) = succ(succ(a' + b)) [add_succ_left], end

add_comm :: forall a : N, forall b : N => a + b = b + a proof case 0 => 0 + b = b [add_zero_left], b + 0 = b [add_zero_right], case succ(a') => succ(a') + b = succ(a' + b) [add_succ_left], b + succ(a') = succ(b + a') [add_succ_right] = succ(a' + b) [IH], end ```