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 * now looking at trying to do the { x = 1, y = x } : { x : I32, y : I32 } thing 😅
brendanzab might have to roll back my thing where you can construct records with out of order fields
matrixbot
@matrixbot
brendanzab Kind of wish I could have something like Tuple [ I32, String ] == { 0 : I32, 1 : I32 }
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 ]
matrixbot
@matrixbot
brendanzab re. the unordered construction - they issue is that I have a btreemap for my record terms
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
matrixbot
@matrixbot
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
matrixbot
@matrixbot
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 😭
matrixbot
@matrixbot
brendanzab hehehe
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 🤔
matrixbot
@matrixbot
ratmice Yeah, Ur/web is neat it basically allows you to fold over row polymorphic record keys, and like concatenate them if they are disjoint
brendanzab need to attempt to read the 'gentle art of levitation' again
matrixbot
@matrixbot
ratmice Been reading through the compositional compiler correctness things here.
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.