- Join over
**1.5M+ people** - Join over
**100K+ communities** - Free
**without limits** - Create
**your own community**

A friendly little systems language with first-class types. https://github.com/pikelet-lang

- Sep 19 18:03LackingInGrav1tas starred pikelet-lang/pikelet
- Sep 19 07:18nataliepopescu starred pikelet-lang/pikelet
- Sep 13 11:52brendanzab converted_to_draft #222
- Sep 13 11:52brendanzab edited #222
- Sep 13 10:39brendanzab synchronize #222
- Sep 13 04:45brendanzab synchronize #222
- Sep 13 04:38brendanzab synchronize #197
- Sep 13 04:38
brendanzab on next

Use try_iter to avoid blocking Merge pull request #221 from br… (compare)

- Sep 13 04:38brendanzab closed #221
- Sep 13 04:33brendanzab opened #222
- Sep 13 04:32brendanzab opened #221
- Sep 12 19:00blankhart starred pikelet-lang/pikelet
- Sep 12 12:47brendanzab synchronize #197
- Sep 12 12:47
brendanzab on next

Formatting improvements Doc comment improvements Add range information to core l… and 1 more (compare)

- Sep 12 12:47brendanzab closed #220
- Sep 12 12:46brendanzab edited #220
- Sep 12 12:42brendanzab synchronize #220
- Sep 12 12:42brendanzab synchronize #197
- Sep 12 12:42
brendanzab on next

- Sep 12 12:40brendanzab synchronize #197

`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 🤔
`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.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`

`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?
`brendanzab`

heh, fun