1756
https://combot.org/chat/-1001043143583 Ссылки на полезные ресурсы: https://ruhaskell.org/links.html ; Информация о мероприятиях: https://gist.github.com/qnikst/a96cac661be80d126d0829f2ced1916e
в хаскеле же переменные из терма типа вылезают из терма в определение
Читать полностью…
конечно нельзя, они забинжены в типе сигнатуры, там и сидят
Читать полностью…
так что ты хотел сказать-то этим, я не очень понял посыл
Читать полностью…
ну тут у меня знаний не хватает, чтобы чего-то по делу сказать
Читать полностью…
это эргономика простая мне кажется
тут буква а и тут буква а, в человеческой голове — это значит "одна и та же а"
переменные в типе это переменные в типе, это отдельный терм
"где забиндился, там и пригодился"
ну в этом вроде есть смысл, если сигнатуру целиком писать не хочется, она какая-нибудь здоровая и с линзами
Читать полностью…
можно вот так
Definition f {a} (x : a) : Type := a.
это аналог нашего
f @a (x :: a) :: Type = a
если бы так можно было бы написать сейчас
так можно
Definition f : forall a, a -> Type :=
fun a _ => a.
так нельзя, "a" забинжен в типе и никуда не вылезает
Definition f : forall a, a -> Type :=
fun _ _ => a.
Там же тоже есть значащие имена в сигнатурах
Или их нельзя использовать в теле определения?..
эта эргономика потом вылелась в неопределенности в других пропосалах, где стало не ясно, @a патттерн это должен быть матчинг типа, или просто вайлдкард который перебинжевает переменную
Читать полностью…
я не соглашусь с этим, не люблю форолы, и вообще не понимаю почему переменные из сигнатуры протекают вниз
Читать полностью…
а это разве не какое-то очень новое расширение в 9.0 или типа того?
Читать полностью…
можно и без форала, просто биндить в паттернах, а не в сигнатуре
Читать полностью…