IK
Size: a a a
2020 May 18
АГ
А кто-нибудь использует liquid haskell? если нет, то почему?
NI
А кто-нибудь использует liquid haskell? если нет, то почему?
Это отдельный от хаскеля язык.
С остальным хаскелем он почти никак не сочетается, кроме самых простых функций.
С остальным хаскелем он почти никак не сочетается, кроме самых простых функций.
АГ
Это отдельный от хаскеля язык.
С остальным хаскелем он почти никак не сочетается, кроме самых простых функций.
С остальным хаскелем он почти никак не сочетается, кроме самых простых функций.
а в чем выражается несочетаемость? это же просто отдельный тайпчекер с сигнатурами в комментах (насколько я понял этот синтаксис, для хаскель компилера это комменты)
NI
а в чем выражается несочетаемость? это же просто отдельный тайпчекер с сигнатурами в комментах (насколько я понял этот синтаксис, для хаскель компилера это комменты)
Например, классы типов из хаскеля не перетащишь.
АГ
Например, классы типов из хаскеля не перетащишь.
вы имеете в виду что у него недостаточная выразительная сила? типа он может только в совсем простые вещи? или то что на сложном коде в котором используются хитрые конструкции он ломается?
NI
Это прикольная концепция.
Но язык Liquid Haskell, во многом, сильно другой.
И годится ли он для "большого" программирования, это большой вопрос.
Какие-то мелкие вещи на нём вполне ничотак делать.
Но язык Liquid Haskell, во многом, сильно другой.
И годится ли он для "большого" программирования, это большой вопрос.
Какие-то мелкие вещи на нём вполне ничотак делать.
NI
вы имеете в виду что у него недостаточная выразительная сила? типа он может только в совсем простые вещи? или то что на сложном коде в котором используются хитрые конструкции он ломается?
Насчёт выразительной силы, вопрос открытый, там есть другие конструкции.
Но навскидку, довольно-таки убедительным видится, что многое из хаскеля там внутри не описывается.
Но навскидку, довольно-таки убедительным видится, что многое из хаскеля там внутри не описывается.
NI
Хорош он тем, что многие вещи в нём доказываются автоматически.
Но на этом, пожалуй, достоинств больше и не вижу ;-)
Сама система доказательств сильно другая, по сравнению с зависимыми типами.
Его можно сравнить с Ms Dafny (только тут ещё и императивное).
Но на этом, пожалуй, достоинств больше и не вижу ;-)
Сама система доказательств сильно другая, по сравнению с зависимыми типами.
Его можно сравнить с Ms Dafny (только тут ещё и императивное).
LO
Руками инстанс написать будет ещё короче
R:
Как на TH написать такое? У меня пока только более простые примеры получаются
https://gist.github.com/DoctorRyner/bae945d97d58ffa6a7afc8b8f81d8794
https://gist.github.com/DoctorRyner/bae945d97d58ffa6a7afc8b8f81d8794
R:
а что такое
Mesh, откуда доставать значение?Мои биндинги к babylonjs https://github.com/DoctorRyner/babylon/blob/master/src/Babylon/Mesh/Types.hs
R:
линзы не делают то же самое через th?
Ну, было бы хорошо
R:
Просто я не особо еще линзы знаю