| 5 Jul 2022 |
 Gabriel Barreto | We've been using Zulip instead of Element | 22:17:32 |
 Zyansheep | Can I join the zulip? | 22:19:18 |
| Gabriel Barreto | I'm pretty sure it's open, you just have to create an account | 22:19:46 |
| Zyansheep | its telling me I need an invitation... | 22:21:31 |
| Zyansheep | 
Download Screenshot_20220705_182212.png | 22:22:20 |
| Zyansheep | pops up when I press "Sign Up" or when I press "Log in with Github" | 22:22:42 |
| Gabriel Barreto | Oh it's still not public, sorry about that. We're eventually going to open it | 22:25:51 |
| Gabriel Barreto | That's pretty cool, I wanna learn more about this, since it avoids some of the issues with self types | 22:27:01 |
| Zyansheep | In reply to @yatima-gb:matrix.org
Oh it's still not public, sorry about that. We're eventually going to open it any chance I can get an invitation? my github is zyansheep. I would like to be apart of the conversation : ) | 22:31:13 |
| Zyansheep | In reply to @yatima-gb:matrix.org
Oh it's still not public, sorry about that. We're eventually going to open it * any chance I can get an invitation? my github is zyansheep. I would like to be apart of the conversation : )
edit: thx | 22:33:19 |
| Gabriel Barreto | Hmm how do you prove induction though? | 23:05:28 |
| 6 Jul 2022 |
 pomone08 | Induction happens when a scrutinee of a split expression or a match expression reduces to a variable | 12:22:37 |
| pomone08 | In that case, we find all occurrences of that variable in the context and replace it with the pair in a split expression or a label in a match expression | 12:23:16 |
| pomone08 | But you can also have a function for it like you have with self types, but now the type you are mentioning is not itself | 12:23:53 |
| pomone08 | nat_ind : (P: Nat -> Type) -> (P zero) -> ((n: Nat) -> P (succ n)) -> (scrutinee: Nat) -> P scrutinee
| 12:25:24 |
| pomone08 | Where
Nat : Type;
Nat =
(label: { zero succ }) !> match label {
|zero| Unit;
|succ| Nat;
};
zero : Nat;
zero =
:zero, unit;
succ : Nat -> Nat;
succ = value =>
:succ, value;
| 12:26:07 |
| pomone08 | Also, I think I might need an invitation for Zulip | 12:26:24 |
| pomone08 | * nat_ind : (P: Nat -> Type) -> (P zero) -> ((n: Nat) -> P (succ n)) -> (scrutinee: Nat) -> P scrutinee;
| 12:27:31 |
| pomone08 | * Where
Unit : Type;
Unit =
{ unit };
unit : Unit;
unit =
:unit;
Nat : Type;
Nat =
(label: { zero succ }) !> match label {
|zero| Unit;
|succ| Nat;
};
zero : Nat;
zero =
:zero, unit;
succ : Nat -> Nat;
succ = value =>
:succ, value;
| 12:28:04 |
| pomone08 | * nat_ind : (P: Nat -> Type) -> (P zero) -> ((n: Nat) -> P (succ n)) -> (scrutinee: Nat) -> P scrutinee;
nat_ind = P => p_zero => p_succ => scrutinee =>
split scrutinee {|label, scrutinee| match label {
|zero| p_zero;
|succ| p_succ scrutinee;
}};
| 12:30:25 |
| pomone08 | * nat_ind : (P: Nat -> Type) -> (P zero) -> ((n: Nat) -> P (succ n)) -> (scrutinee: Nat) -> P scrutinee;
nat_ind = P => p_zero => p_succ => scrutinee =>
split scrutinee {|label, scrutinee| match label {
|zero| p_zero;
|succ| p_succ scrutinee;
}};
| 12:32:50 |
| Gabriel Barreto | Hmm I think I get it. So when you're checking/inferring `split x {|a, b| e}` and `x` is a variable, you add `a` and `b` to the context, substitute all instances of `x` with `(a, b)` and proceed to check/infer `e` | 13:56:55 |
| Gabriel Barreto | * Hmm I think I get it. So when you're checking/inferring split x {|a, b| e} and x is a variable, you add a and b to the context, substitute all instances of x with (a, b) and proceed to check/infer e | 13:58:00 |
| Gabriel Barreto | * Hmm I think I get it. So when you're checking/inferring split x {|a, b| e} and x is a variable, you add a and b to the context right before x (do you also remove x from the context?), substitute all instances of x with (a, b) in the context and proceed to check/infer e | 13:59:14 |
| Gabriel Barreto | * Hmm I think I get it. So when you're checking/inferring split x {|a, b| e} and x is a variable of type (a : A) :> B, you add a : A and b : B to the context right before x (do you also remove x from the context?), substitute all instances of x with (a, b) in the context and proceed to check/infer e | 14:03:59 |
| Gabriel Barreto | * Hmm I think I get it. So when you're checking/inferring split x {|a, b| e} and x is a variable of type (a : A) !> B, you add a : A and b : B to the context right before x (do you also remove x from the context?), substitute all instances of x with (a, b) in the context and proceed to check/infer e | 14:05:01 |
| Gabriel Barreto | Similarly, when checking match x { |a| e1; |b| e2; } then x must be a variable of type {a b} (from what I understood, a and b here are actually symbols :a and :b), then you must check two expressions: e1 with :a in place of x in the context, and e2 with :b in place of x in the context | 14:09:10 |
| Gabriel Barreto | Really cool idea. I've always thought that it was a good idea to add labels to the lambda calculus, which makes it quite similar to a pure Lisp (only symbols, pairs and lambdas), so that datatypes are a pair symbol + rest, though I couldn't quite get it right | 14:12:18 |
| pomone08 | Yes, that is exactly the idea behind the type checker | 15:56:40 |
| Gabriel Barreto | I guess you can extend label types to have any number of labels | 15:58:47 |
