Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • Oct 22 09:14
    LPeter1997 starred pikelet-lang/pikelet
  • Oct 21 08:40
    brendanzab edited #196
  • Oct 20 09:58
    brendanzab edited #196
  • Oct 20 09:01
    brendanzab synchronize #197
  • Oct 20 09:01

    brendanzab on next

    Remove editor highlighting work… (compare)

  • Oct 18 06:30
    brendanzab synchronize #197
  • Oct 18 06:30

    brendanzab on next

    Add TODO comments to REPL (compare)

  • Oct 17 09:49
    brendanzab edited #196
  • Oct 17 09:49
    brendanzab synchronize #197
  • Oct 17 09:48

    brendanzab on next

    Move back to using mdBook for d… Merge pull request #232 from br… (compare)

  • Oct 17 09:48
    brendanzab closed #232
  • Oct 17 09:16
    brendanzab synchronize #232
  • Oct 17 09:11
    brendanzab ready_for_review #232
  • Oct 17 09:11
    brendanzab synchronize #232
  • Oct 17 08:52
    brendanzab synchronize #232
  • Oct 14 19:55
    figsoda starred pikelet-lang/pikelet
  • Oct 12 08:56
    brendanzab synchronize #232
  • Oct 12 04:33
    LXSMNSYC starred pikelet-lang/pikelet
  • Oct 11 08:30
    brendanzab edited #232
  • Oct 11 07:15
    brendanzab synchronize #232
matrixbot
@matrixbot
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
matrixbot
@matrixbot
segeljakt do you know any good resources on declarative programming?
matrixbot
@matrixbot
segeljakt btw, have you seen this language? https://www.minizinc.org/
brendanzab yeah I've heard of it!
brendanzab never played around with it though
matrixbot
@matrixbot
brendanzab Was messing around with this today :P pikelet-lang/pikelet#222
brendanzab dunno if it is worth it though haha
matrixbot
@matrixbot

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.p
  • 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 * 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
matrixbot
@matrixbot
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
matrixbot
@matrixbot
atennapel For now, I just added an unsafe equality elimination that allows the equality to be erased. For Pikelet you can do this erasure safely, if you remain consistent, so you will never have these issues.
atennapel Maybe I can hide the unsafety in some kind of module, using sigma types 🤔
matrixbot
@matrixbot
segeljakt Random shower thought: a rust macro which you put around your AST data structure for generating different versions for different passes of the compiler
segeljakt If you need to for example replace symbolic identifiers with resolved identifiers
brendanzab kind of like nanopass.org?
matrixbot
@matrixbot
segeljakt Hmmm, I don't know, I was just thinking about something which you put on your rust struct or enum that generates multiple versions of them where some fields/variants have different types in each version, maybe you could do it with generics though
matrixbot
@matrixbot
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
matrixbot
@matrixbot
brendanzab wish we had something similar for Rust
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?
matrixbot
@matrixbot
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
matrixbot
@matrixbot
segeljakt What stuff should an AST be generic over?
matrixbot
@matrixbot
brendanzab Got some better literal handling now! pikelet-lang/pikelet#223
matrixbot
@matrixbot
brendanzab really need a better test harness so that I can start doing failing tests 😭
matrixbot
@matrixbot
ratmice I'd be interested in trying to stuff the float parsing into json-pop and run it through json-bench, Its float parsing is basically the only thing not on par with other parsers, its currently using lexical.
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?
matrixbot
@matrixbot
ratmice I'm not sure, haven't looked into it too much, but I haven't seen anything (public in there) that doesn't take a whole buffer, so you have to get to the end of the number before you start converting. It seems like what you implemented implements it digit at a time
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