A friendly little systems language with first-class types. https://github.com/pikelet-lang
brendanzab on main
Remove lifts from specification Cleanup specification of lexica… Elide explicit lifetimes and 1 more (compare)
brendanzab on main
Remove universe levels for now … Merge pull request #240 from br… (compare)
brendanzab on main
Rework local variable API and i… Remove local_levels vector in e… Merge pull request #239 from br… (compare)
brendanzab
* This was pretty cool - using multi-stage programming to eliminate the runtime overhead of datatype generic programming: https://www.youtube.com/watch?v=vK_cg8UP6gU
suhr
Kinda strange, it's like a young dinosaur that still lives today.
brendanzab
now looking at trying to do the '{ x = 1, y = x } : { x : I32, y : I32 }` thing 😅
brendanzab
* now looking at trying to do the { x = 1, y = x } : { x : I32, y : I32 }
thing 😅
brendanzab
And Array 3 I32 == { 0 : I32, 1 : I32, 2 : I32 }
brendanzab
also [ 1, 2, 3 ] == { 0 = 1, 1 = 2, 2 = 3 } : Array 3 I32
brendanzab
and [ 23, "hello" ] == { 0 = 23, 1 = "hello" } : Tuple [ I32, String ]
brendanzab
* re. the unordered construction - the issue is that I have a btreemap for my record terms
brendanzab
that lets me have { y = 23, x = 1 } : { x : S32, y : S32 }
brendanzab
because when I type check the term I can pick off entries at my leisure
brendanzab
but that might be getting in the way of other experiements
brendanzab
sorry I realise it might have been confusing that I mentioned that then started talking about another form of ordering - ie. tuples and arrays
ratmice
Yeah, so the way i've been thinking about it is ';' vs ',' where (a, b) specifies the canonical form and ';' canonicalizes based on some convenience like alphabetical order to binding name (or anything), So you get things like [a, b] and [a; b] being like the difference between array, and set
ratmice
It's a bit weird with records, because then "," with records implies some kind of unbalanced raw tree structure or something.
ratmice
Anyhow that might be a way to salvage your existing ordering
brendanzab
interesting - have you seen how logic languages use ;
for 'and' and ,
for 'or'?
brendanzab
eg. Prolog, Mercury, Makam
ratmice
no, I have a kind of weird prolog phobia, something to do with backtracking 😭
brendanzab
I like the logic languages where you get to say whether you backtrack or not
brendanzab
like mercury
brendanzab
but yeah I have pondered using ;
and ,
for or some other symbols like that for types because of that
brendanzab
also been pondering the 'key set' of a record as kind of a finite set or enumeration 🤔
brendanzab
need to attempt to read the 'gentle art of levitation' again
brendanzab
and yeah +1 to Ur/web
brendanzab
nice!
brendanzab
the next 700 compiler correctness theorems
brendanzab
* the next 700 compiler correctness theorems?
ratmice
Yeah, and same authors earlier paper "FabULous Interoperability for ML and a Linear Language"
brendanzab
"FabULous" lmoa
brendanzab
yeah I've heard of it!
brendanzab
never played around with it though
brendanzab
dunno if it is worth it though haha
atennapel
> <@atennapel:matrix.org> Well I implemented Nat, Fin and (indexed) Fix, here are vectors: https://github.com/atennapel/tinka/blob/master/lib/vec.p
> VCons 1 (VCons 2 (VCons 3 VNil))
type: Vec (S (S (S Z))) %Nat
term: VCons {%Nat} {S (S Z)} 1 (VCons {%Nat} {S Z} 2 (VCons {%Nat} {Z} 3 (VNil {%Nat})))
norm: (0, %ReflHEq, 1, 0, %ReflHEq, 2, 0, %ReflHEq, 3, 1, %ReflHEq)
atennapel
The norm
is the erased form for a vector of 1, 2, 3. I have to carry around some Refls which is not nice at all...
atennapel
> <@atennapel:matrix.org> Well I implemented Nat, Fin and (indexed) Fix, here are vectors: https://github.com/atennapel/tinka/blob/master/lib/vec.ptype: Vec (S (S (S Z))) %Nat
term: VCons {%Nat} {S (S Z)} 1 (VCons {%Nat} {S Z} 2 (VCons {%Nat} {Z} 3 (VNil {%Nat})))
norm: (0, %ReflHEq, 1, 0, %ReflHEq, 2, 0, %ReflHEq, 3, 1, %ReflHEq)
atennapel
* type: Vec (S (S (S Z))) %Nat
term: VCons {%Nat} {S (S Z)} 1 (VCons {%Nat} {S Z} 2 (VCons {%Nat} {Z} 3 (VNil {%Nat})))
norm: (0, %ReflHEq, 1, 0, %ReflHEq, 2, 0, %ReflHEq, 3, 1, %ReflHEq)
atennapel
* ```
VCons 1 (VCons 2 (VCons 3 VNil))type: Vec (S (S (S Z))) %Nat
term: VCons {%Nat} {S (S Z)} 1 (VCons {%Nat} {S Z} 2 (VCons {%Nat} {Z} 3 (VNil {%Nat})))
norm: (0, %ReflHEq, 1, 0, %ReflHEq, 2, 0, %ReflHEq, 3, 1, %ReflHEq)
```
atennapel
* ```
VCons 1 (VCons 2 (VCons 3 VNil))
type: Vec (S (S (S Z))) %Nat
term: VCons {%Nat} {S (S Z)} 1 (VCons {%Nat} {S Z} 2 (VCons {%Nat} {Z} 3 (VNil {%Nat})))
norm: (0, %ReflHEq, 1, 0, %ReflHEq, 2, 0, %ReflHEq, 3, 1, %ReflHEq)
```