A friendly little systems language with first-class types. https://github.com/pikelet-lang
brendanzab on next
Remove editor highlighting work… (compare)
brendanzab on next
Add TODO comments to REPL (compare)
brendanzab on next
Move back to using mdBook for d… Merge pull request #232 from br… (compare)
brendanzab
ie. in the way of making record construction more like let expressions
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)
```
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...The 0's inbetween is the tag for VCons
and the last 1
is the tag for VNil
atennapel
There is an alternative approach where you define Vec n t
by pattern matching on the n
: case n of { 0 => (); S m => t ** Vec m t }
this removes any tags or indices (and proofs). I have no idea how you can define induction over this though, I just created a post on r/dependent_types to ask for help: https://www.reddit.com/r/dependent_types/comments/iufe6x/induction_after_forcing_and_detagging_in_gentle/
brendanzab
oh yeah seen that before! it's pretty neat
brendanzab
I think something by mcbride or edwin brady?
atennapel
Yeah a paper called "Inductive Families need not store their indices" by McBride Brady and McKinna.
brendanzab
oh yeah you mention it
atennapel
Maybe I can hide the unsafety in some kind of module, using sigma types 🤔
segeljakt
If you need to for example replace symbolic identifiers with resolved identifiers
brendanzab
kind of like nanopass.org?
ratmice
Yeah, does sound a lot like generics, but speaking of nanopass, there was an interesting nanopass talk this year, https://www.youtube.com/watch?v=lqVN1fGNpZw
ratmice
on Implementing the nanopass framework as a nanopass compiler