Agda Боян, не? foxebook.net

дыбр Agda Поставил агду, доказал коммутативность сложения для арифметики Пеано. Мозголомно

Agda Learn You an Agda — williamdemeo.github.io

Coq idris Erlang Agda Haskell *хз
Нужен (не срочно, но час X всё ближе и ближе) экстрактор в ерланг из каких-нибудь зависимых типов. Ничего не нашёл. Есть чо?

Agda Haskell Вышла новая агда. Пруф: wiki.portal.chalmers.se — выглядит весьма годно.

ненужный_пост Agda ? Haskell где почитать про определения bottom (_|_) и top (T) чтобы получить хоть какую-то интуицию по работе с ними, периодически в документации/мануалах они встречаются, но я не уверен, что я все правильно понимаю.

tutorial Agda people.inf.elte.hu Если монадные туториалы стали походить на комиксы, а стрелки больше не вставляют...

Agda При помощи Agda доказывают, что гомотопическая группа окружности — целые числа, видеолекция-введение в HoTT: video.ias.edu
бумажный вариант: cs.cmu.edu

Agda The Decent Way to Learn Functional Programming blog.oxij.org

Agda oxij.org — замечательный сайт @oxij с курсами и заметками по теории типов

Java Coq Agda Haskell sphotos-b.xx.fbcdn.net

бредятина Agda ⨉ : {ℓ ℓ₁ ℓ₂ : Level} {А Б В Г : Set ℓ} →
А ⟪ ℓ₁ ⟫ Б →
В ⟪ ℓ₂ ⟫ Г →
(А × В) ⟪ ℓ₁ ⊔ ℓ₂ ⟫ (Б × Г)
(О ⨉ П) (а , в) (б , г) = О а б × П в г

нувыпонели.

— via bitbucket.org

quote Agda «In Agda, running your program is a sign of weakness»

fp Agda

"Agda ... a dependently typed functional programming language" I think it depends on the number of your PhDs.

via twitter.com

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 - язык простой и красивый

math fp categories Agda web.student.chalmers.se github.com gitorious.org — category theory in Agda

Agda ? programming Настолько ли неудобно писать на agda, как говорят?
Поскольку это ЯП (в том числе), для написания каких приложений он хорошо подходит?

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

Agda Haskell programming perikov.livejournal.com — пока одни в очередной раз доказывают практическую применимость монад, другим в рамках Haskell уже становится тесно