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)
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
brendanzab
segeljakt: have you seen 'trees that grow' for haskell?
brendanzab
but yeah I was more thinking of the def-language
side of nanopass
brendanzab
* but yeah I was more thinking of the define-language
side of nanopass https://docs.racket-lang.org/nanopass/index.html#%28form._%28%28lib._nanopass%2Fbase..rkt%29._define-language%29%29
brendanzab
where you can add to and alter languages
brendanzab
might also be interesting to look at Ornaments?
ratmice
I once tried to implement it in Ur's typelevel meta-programming stuff, its always seemed quite difficult to pull off the whole thing in a statically typed setting...
brendanzab
heh, fun
ratmice
The thing that it seems to be is just iterating over each character twice, and then again in lexical, I guess it depends on the morph stuff perhaps
brendanzab
ahh... do any of the config things in lexical-core
help at all?
ratmice
But its certainly probably worth looking at the guts, I just don't think any of that is public there
ratmice
Its interesting it seems that the callback changes in Logos
change how you need to approach it.
brendanzab
yeah that's why I haven't used it
brendanzab
my colleague was like 'surely this is solved'?
brendanzab
but yeah I really want something that I can decide the syntax of
brendanzab
and have it deal with the decoding
ratmice
Also, there is some discussion here of streaming float parsing in this serde issue, Alexhuszagh/rust-lexical#28 In that issue he made a minimal-lexical crate which might be a better an easier starting point for understanding lexical.
ratmice
sorry, wrong bug
ratmice
* serde-rs/json#536
karroffel
Does the next
branch have some way to encode enums/ADTs yet? I see everything is built around modules so far which is really cool
karroffel
just curious how to base ADTs on records 🙃
brendanzab
yeah, need to add that
brendanzab
was going to use finite sets to let you describe the 'tags'
brendanzab
and then let you dependently eliminate them