Чтобы добавлять сообщения и комментарии, .

@ymn:
ymn

Боян, не? foxebook.net

@PineappleZombie:
PineappleZombie

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

@ymn:
ymn

Learn You an Agda — williamdemeo.github.io

@Zert:
Zert

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

@ymn:
ymn

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

@qnikst:
qnikst

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

@trapdoor:
trapdoor

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

@dukkha:
dukkha

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

@dukkha:
dukkha

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

@jtootf:
jtootf

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

@qrilka:
qrilka

sphotos-b.xx.fbcdn.net

@iportnov:
iportnov

: {ℓ ℓ₁ ℓ₂ : Level} {А Б В Г : Set ℓ} →
А ⟪ ℓ₁ ⟫ Б →
В ⟪ ℓ₂ ⟫ Г →
(А × В) ⟪ ℓ₁ ⊔ ℓ₂ ⟫ (Б × Г)
(О ⨉ П) (а , в) (б , г) = О а б × П в г

нувыпонели.

— via bitbucket.org

@PineappleZombie:
PineappleZombie

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

@jtootf:
jtootf

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

@jtootf:
jtootf

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

@jtootf:
jtootf

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

@4DA:
4DA

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

@klapaucius:
klapaucius

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

@jtootf:
jtootf

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