Zert
Erlang Haskell Agda Coq idris *хз
Нужен (не срочно, но час X всё ближе и ближе) экстрактор в ерланг из каких-нибудь зависимых типов. Ничего не нашёл. Есть чо?
qnikst
? Haskell Agda ненужный_пост где почитать про определения bottom (_|_) и top (T) чтобы получить хоть какую-то интуицию по работе с ними, периодически в документации/мануалах они встречаются, но я не уверен, что я все правильно понимаю.
dukkha
Agda При помощи Agda доказывают, что гомотопическая группа окружности — целые числа, видеолекция-введение в HoTT: video.ias.edu
бумажный вариант: cs.cmu.edu
jtootf
code fp Agda
_∘_ : {A : Set}{B : A -> Set}{C : (x : A) -> B x -> Set}
      (f : {x : A}(y : B x) -> C x y)(g : (x : A) -> B x)
      (x : A) -> C x (g x)
(f ∘ g) x = f (g x)

Agda - язык простой и красивый
4DA
? programming Agda Настолько ли неудобно писать на agda, как говорят?
Поскольку это ЯП (в том числе), для написания каких приложений он хорошо подходит?
klapaucius
ml csharp fsharp Agda Земную жизнь пройдя до середины, я очутился в жизненной ситуации, которая заставляет меня изучить *fsharp. Это, конечно, полуправда. Никто заставлять изучать F# не станет, но если можно писать на работе на нем, а не на *csharp — то почему бы и нет? Уж если приходится есть пирожки с булавками — пусть они будут хотя бы английскими. Не пирожки, а булавки, конечно. Такой оптимизм основан на том, что я поверхностно знаком с "функциональными языками" *ml семейства и примерно представляю, чего от них ожидать. Чтоб смыть железное послевкусие булавок, я параллельно продегустирую что-нибудь заведомо приятное, *agda 2, например.