Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
Labbekak#0369
@_discord_84011264606502912:t2bot.io
[m]
Is that the same as first class signatures? Like https://github.com/agda/agda-stdlib/blob/master/src/Data/Record.agda ?
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
yeah, I think so
but yeah you'd hope a bit less cursed to use in practice
Labbekak#0369
@_discord_84011264606502912:t2bot.io
[m]
Could use some nicer syntax yes
Labbekak#0369
@_discord_84011264606502912:t2bot.io
[m]
But semantics look solid
atlx#6478
@_discord_285578743324606482:t2bot.io
[m]
:thinkong:
Labbekak#0369
@_discord_84011264606502912:t2bot.io
[m]

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
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
why the bools?
AndrasKovacs#1295
@_discord_524955176302411776:t2bot.io
[m]
for sum type description
Labbekak#0369
@_discord_84011264606502912:t2bot.io
[m]
Indeed
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
instead of the labels?
Labbekak#0369
@_discord_84011264606502912:t2bot.io
[m]
Yeah, just for simplicity
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
atlx#6478
@_discord_285578743324606482:t2bot.io
[m]
Wait whut
Labbekak#0369
@_discord_84011264606502912:t2bot.io
[m]
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
woah, it was recorded
tk#1172
@_discord_343549617729699842:t2bot.io
[m]
I thought ppl here would find it interesting
way beyond me lol but still cool to read
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
tk this looks interesting too https://danilafe.com/blog/coq_dawn/
tk#1172
@_discord_343549617729699842:t2bot.io
[m]
This is so cool
All syntax is macros, so you can create a really expressive language to describe your domain model
smt#5396
@_discord_85481381928382464:t2bot.io
[m]
that's really cool, i wonder what the list of builtin macros looks like
tk#1172
@_discord_343549617729699842:t2bot.io
[m]
also another cool pl
bh#3738
@_discord_316903914941186048:t2bot.io
[m]
Finally got copies of HtDP and The $foo Schemer!
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
woot
what is a $foo
I have the little schemer
did you get the reasoned schemer too?
bh#3738
@_discord_316903914941186048:t2bot.io
[m]
Little, Reasoned, Seasoned
quiet_laika
@quiet_laika:matrix.org
[m]
the Wizened Schemer
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
thoughtful schemer
tk#1172
@_discord_343549617729699842:t2bot.io
[m]
What is the name of the proof that a Type can’t be its own Type?
AndrasKovacs#1295
@_discord_524955176302411776:t2bot.io
[m]
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
AndrasKovacs#1295
@_discord_524955176302411776:t2bot.io
[m]
ratmice
@ratmice:matrix.org
[m]
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
1 reply
ratmice
@ratmice:matrix.org
[m]
footnote 5 is hilarious
tk#1172
@_discord_343549617729699842:t2bot.io
[m]
Thanks!
brendanzab#6008
@_discord_280132690059984897:t2bot.io
[m]
hehe yeah
The creator also made this neat website: http://liamoc.net/holbert
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