A friendly little systems language with first-class types. https://github.com/pikelet-lang
Is that the same as first class signatures? Like https://github.com/agda/agda-stdlib/blob/master/src/Data/Record.agda ?
(clickable version https://agda.github.io/agda-stdlib/README.Data.Record.html)
but yeah you'd hope a bit less cursed to use in practice
Yay I managed to implement "Gentle art of levitation", including the levitation part. I had to change to a bidirectional core language to make it work. Here is the description of Descriptions in its full beauty:
DescD =
ConD^ (False^2, True^2, Bool^, \x. (elim BoolDesc^) (ConD^ (True^2, Unit^2))
(ConD^ (False^2, True^2, Bool^, \x. (elim BoolDesc^)
(ConD^ (False^2, True^2, Type, \x. ConD^ (False^2, False^2, False^2, Lift lower x, ConD^ (True^2, Unit^2), Unit^2), Unit^2))
(ConD^ (False^2, True^2, Bool^, \x. (elim BoolDesc^) (ConD^ (False^2, False^2, True^2, ConD^ (True^2, Unit^2), Unit^2))
(ConD^ (False^2, True^2, Type, \x. ConD^ (False^2, False^2, True^2, ConD^ (True^2, Unit^2), Unit^2), Unit^2)) (lower x), Unit^2)) (lower x), Unit^2)) (lower x), Unit^2);😅
All the
^ and ^2 noise is the lifting from the universe hierarchy
Makes it even more unreadable though
The above is the normalized form of:
DescD : Desc^ =
SumD^ End^ ( -- End : Desc
SumD^ (Arg^ Type (\A. HInd^ (Lift A) End^)) ( -- Arg : (A : Type) -> (A -> Desc) -> Desc
SumD^ (Ind^ End^) -- Ind : Desc -> Desc
(Arg^ Type (\_. Ind^ End^)))); -- HInd : Type -> Desc -> Desc
The Gentle Art of Levitation: https://www.irif.fr/~dagand/papers/levitation.pdf https://vimeo.com/16534403
I thought ppl here would find it interesting
way beyond me lol but still cool to read
This is so cool
All syntax is macros, so you can create a really expressive language to describe your domain model
that's really cool, i wonder what the list of builtin macros looks like
also another cool pl
what is a $foo
I have the little schemer
did you get the reasoned schemer too?
What is the name of the proof that a Type can’t be its own Type?
There are several different proofs. Girard's paradox is the oldest, but it's complicated. Hurkens' paradox simplifies it a lot. Russell's paradox is extremely simple, but it requires inductive types, while the former two proofs only require Pi + some other basic stuff that I don't exactly remember
1 reply
The creator also made this neat website: http://liamoc.net/holbert
I had a go at trying to implement some dependent type theory stuff in it: http://liamoc.net/holbert/?https://gist.githubusercontent.com/brendanzab/1b4732179b15201bf33fed6dbca02458/raw/mltt.holbert#anchor85
Edit: I had a go at trying to implement some dependent type theory stuff in it: http://liamoc.net/holbert/?https://gist.githubusercontent.com/brendanzab/1b4732179b15201bf33fed6dbca02458/raw/mltt.holbert