-
Notifications
You must be signed in to change notification settings - Fork 6
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Is help needed? #1
Comments
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? |
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? |
I should be available as @0xd34df00d on tg, I think (I don't have much experience with it).
Без проблем :) |
Не смог найти Вас в телеграмме. Буду писать здесь (или же если вам нравится другой формат общения, напишите). У вас в Readme.md разметка eBNF испортилась, поскольку Вы используете неправильную версию eBNF (вот ссылка на примеры правильной грамматики eBNF для подсветки в code блоках). Также по поводу 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 Было бы идеально сделать Есть еще предложение сделать Помощь в виде pull requests для исправления мест |
А давайте ваш аккаунт, я попробую вас найти. Ну и сейчас, конечно, мало кто пользуется XMPP, но там я тоже есть. Но можно и в телеграме, да. За фикс с README спасибо, я сходу не смог добиться правильной подсветки, и решил не тратить на это много времени. Спасибо, что поправили, так гораздо лучше!
Да, это тоже хорошее замечание. Думаю, поменяю.
А это интересный взгляд! Как бы refinements как конструкции первого класса могли бы выглядеть и себя вести?
Это хорошая идея.
Уф, я боюсь, что на этом этапе это будет скорее тратой времени. Код-то одноразовый на поэкспериментировать с реализацией и пощупать её вживую, в идеале хотелось бы потом всё это выкинуть и, например, сделать компиляцию liquid haskell в dependent haskell (который, надеюсь, уже скоро появится). С пейпером у меня есть некий план действий, но по нему часть этих тудушек вообще будет выкинута, как и соответствующие куски. Наверное, самой лучшей помощью по пейперу сейчас будет прикинуть, как можно сделать dependent pattern matching (с передачей в «обработчики» разных конструкторов доказательства равенства терма, по которому идёт паттерн-матчинг, соответствующему конструктору, применённому к данным в паттерне) в обычном calculus of constructions — что-то вроде Boehm-Berarducci encoding, но с этим самым доказательством равенства. Я над этим поломал голову несколько дней и ни к чему разумному не пришёл и уже всерьёз думаю расширять CoC примитивной конструкцией для такого матчинга, но всё же хотелось бы по возможности целевой язык, в который refinement'ы компилируются, держать минимальным. В обозримом, надеюсь, будущем (через недельку-две) будет очень полезно, если вы просто попробуете статью почитать и сказать, понятна ли она для кого-нибудь, кроме её непосредственного автора, ну и в идеале нет ли там каких-то очевидных ошибок. |
Скорее всего, приближенно к замыканиям. refinement должен "захватить" внешние переменные от которых он зависит, и нести с собой, подобно замыканию. При этом он имеет тип biggerThan: Int -> Type
biggerThan x = { v : Int | v > x } -- Здесь захватывается переменная x
foo: biggerThan 5 -> Int
bar: Int
bar = foo 10 -- Здесь для доказательства используется захваченное ранее число 5
Не совсем ясна мысль, можно привести пример? Вы хотите сделать возможность указывать refinements для вложенных в algebraic data types типов полей? data Foo = MkFoo Int
bar: { v: Foo | {- здесь указать что требуется уточненное значение Int из MkFoo? -} }
Ок. |
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.
The text was updated successfully, but these errors were encountered: