pikelet/Lobby

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

matrixbot

@matrixbot

ratmice no, I have a kind of weird prolog phobia, something to do with backtracking 😭

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.

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?

Where communities thrive

People

Repo info

Activity