Is help needed?

[p0lunin]

Hello. I am developing toy functional language with dependent/refinement types. I found your ideas to be very similar to my own. So if you need i would gladly help in implementing your language.

[0xd34df00d]

Hey! I'm super glad this sparks interest, and nice to see somebody with similar ideas!

Right now I'm working on formalizing the language and proving that it actually "makes sense". Is that something that's on your roadmap?

[p0lunin]

Yes, i thought about formalization and proofing that it make sense in future. Do you have an account in messenger like Telegram/Discord? I think it will be more convenient to communicate there. And would you mind if we communicate in Russian?

[0xd34df00d]

Do you have an account in messenger like Telegram/Discord?

I should be available as @0xd34df00d on tg, I think (I don't have much experience with it).

And would you mind if we communicate in Russian?

Без проблем :)

[p0lunin]

Не смог найти Вас в телеграмме. Буду писать здесь (или же если вам нравится другой формат общения, напишите).

У вас в Readme.md разметка eBNF испортилась, поскольку Вы используете неправильную версию eBNF (вот ссылка на примеры правильной грамматики eBNF для подсветки в code блоках). Поэтому предлагаю исправить синтаксис на правильную версию (done), либо же можно заменить eBNF на другую форму, например ANTLR. Могу этим заняться.

Также по поводу readme, второй пример отсюда про ко(нтра)вариантивность кажется непоказательным. Из-за большого количества скобок сплывается сигнатура в одно целое, разделить на части затруднительно. Также плохо заметна разница между > и >= из-за, опять же, большого количества скобок. Думаю, что можно переделать его например на:

f : { v : Int | v > 5 } -> { v : Int | v > -2 }

g : ({ v : Int | v > -2 } -> { v : Int | v > 5 }) -> { v : Int | v >= 0 }

h : { v : Int | v >= 0 }
h = g f

Было бы идеально сделать { v : Int | v > x } функцией, но я смотрю по синтаксису что refinements не являются first-class конструкциями?

Есть еще предложение сделать v (или self/this/val) в refinement ключевым словом, чтобы не было необходимости писать везде бойлерплейт { v : ... }.

Помощь в виде pull requests для исправления мест TODO в коде и пейпере нужна?

[0xd34df00d]

А давайте ваш аккаунт, я попробую вас найти. Ну и сейчас, конечно, мало кто пользуется XMPP, но там я тоже есть. Но можно и в телеграме, да.

За фикс с README спасибо, я сходу не смог добиться правильной подсветки, и решил не тратить на это много времени. Спасибо, что поправили, так гораздо лучше!

Из-за большого количества скобок сплывается сигнатура в одно целое, разделить на части затруднительно. Также плохо заметна разница между > и >= из-за, опять же, большого количества скобок.

Да, это тоже хорошее замечание. Думаю, поменяю.

Было бы идеально сделать { v : Int | v > x } функцией, но я смотрю по синтаксису что refinements не являются first-class конструкциями?

А это интересный взгляд! Как бы refinements как конструкции первого класса могли бы выглядеть и себя вести?

Есть еще предложение сделать v (или self/this/val) в refinement ключевым словом, чтобы не было необходимости писать везде бойлерплейт { v : ... }.

Это хорошая идея.

Помощь в виде pull requests для исправления мест TODO в коде и пейпере нужна?

Уф, я боюсь, что на этом этапе это будет скорее тратой времени.

Код-то одноразовый на поэкспериментировать с реализацией и пощупать её вживую, в идеале хотелось бы потом всё это выкинуть и, например, сделать компиляцию liquid haskell в dependent haskell (который, надеюсь, уже скоро появится).

С пейпером у меня есть некий план действий, но по нему часть этих тудушек вообще будет выкинута, как и соответствующие куски.

Наверное, самой лучшей помощью по пейперу сейчас будет прикинуть, как можно сделать dependent pattern matching (с передачей в «обработчики» разных конструкторов доказательства равенства терма, по которому идёт паттерн-матчинг, соответствующему конструктору, применённому к данным в паттерне) в обычном calculus of constructions — что-то вроде Boehm-Berarducci encoding, но с этим самым доказательством равенства.

Я над этим поломал голову несколько дней и ни к чему разумному не пришёл и уже всерьёз думаю расширять CoC примитивной конструкцией для такого матчинга, но всё же хотелось бы по возможности целевой язык, в который refinement'ы компилируются, держать минимальным.

В обозримом, надеюсь, будущем (через недельку-две) будет очень полезно, если вы просто попробуете статью почитать и сказать, понятна ли она для кого-нибудь, кроме её непосредственного автора, ну и в идеале нет ли там каких-то очевидных ошибок.

[p0lunin]

https://t.me/f0land

А это интересный взгляд! Как бы refinements как конструкции первого класса могли бы выглядеть и себя вести?

Скорее всего, приближенно к замыканиям. refinement должен "захватить" внешние переменные от которых он зависит, и нести с собой, подобно замыканию. При этом он имеет тип Type 1, так как используется таким же способом что и Type 1.

biggerThan: Int -> Type
biggerThan x = { v : Int | v > x } -- Здесь захватывается переменная x

foo: biggerThan 5 -> Int

bar: Int
bar = foo 10 -- Здесь для доказательства используется захваченное ранее число 5

Наверное, самой лучшей помощью по пейперу сейчас будет прикинуть, как можно сделать dependent pattern matching (с передачей в «обработчики» разных конструкторов доказательства равенства терма, по которому идёт паттерн-матчинг, соответствующему конструктору, применённому к данным в паттерне) в обычном calculus of constructions — что-то вроде Boehm-Berarducci encoding, но с этим самым доказательством равенства.

Не совсем ясна мысль, можно привести пример? Вы хотите сделать возможность указывать refinements для вложенных в algebraic data types типов полей?

data Foo = MkFoo Int

bar: { v: Foo | {- здесь указать что требуется уточненное значение Int из MkFoo? -} }

В обозримом, надеюсь, будущем (через недельку-две) будет очень полезно, если вы просто попробуете статью почитать и сказать, понятна ли она для кого-нибудь, кроме её непосредственного автора, ну и в идеале нет ли там каких-то очевидных ошибок

Ок.