deniok: (Рыжий)
Очень заманчивая идея о том, как в Agda загнать под капот навязчивые subst и cong. Пример от автора.
deniok: (ухмыляюсь)
Что-то попытки подключить к Агде унивалентность (отключив аксиому K) приводят к еженедельному обнаружению дырок в паттерн-матчинге. Вот опять сообщают. Следите за рассылкой, оставайтесь на острие.
deniok: (ухмыляюсь)
К вопросу о заселении ⊥ при включенном type-in-type. Делается прямой реализацией парадокса Рассела
{-# OPTIONS --type-in-type --without-K #-} 
module russell where

open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Empty

-- a model of set theory
data U : Set where
  set : (I : Set) → (I → U) → U

-- a set is regular if it doesn't contain itself
regular : U → Set
regular (set I f) = (i : I) → ¬ (f i ≡ set I f)

-- Russell's set: the set of all regular sets
R : U
R = set (Σ U regular) proj₁

-- R is not regular
R-nonreg : ¬ (regular R)
R-nonreg reg = reg (R , reg) refl

-- R is regular
R-reg : regular R
R-reg (x , reg) p = subst regular p reg (x , reg) p

-- contradiction
absurd : ⊥
absurd = R-nonreg R-reg
Взято отсюда:
http://www.reddit.com/r/compsci/comments/1a7g6q/a_question_on_set_classes_and_dependent_types/
http://article.gmane.org/gmane.comp.lang.agda/5002
http://hpaste.org/84029
deniok: (Рыжий)
Эти ваши интернеты бурлят:

ru-marazm.livejournal.com/3591670.html

lj.rossia.org/users/tiphareth/1685303.html

Агда, кстати, на стороне внучки, 9 раз по 2 литра будет 9 * 2:
_*_ : ℕ → ℕ → ℕ
zero  * n = zero
suc m * n = n + (m * n)
Впрочем внучке стоило бы снять все вопросы, предоставив доказательство
*-commutative : ∀ m n → m * n ≡ n * m
Взяв его, например, из Data.Nat.Properties. Или получив самостоятельно.

deniok: (lambda cube)
 
В современной теории типов выделяют два основных класса равенств: Definitional equality и Propositional equality. 
 
Ого! Ну-ка, ну-ка... )
deniok: (typed lambda)
 Ян [livejournal.com profile] oxij  написал Жёсткое введение в зависимые типы на Агде. Не могу не пропиарить. Открывайте и изучайте, свиньи вы эдакие (кроме, конечно, девушек) (c) r_l

UPD: обсуждение в Твиттере

deniok: (ухмыляюсь)
Как можно конструктивно доказать, что число 4 является полным квадратом некоторого натурального числа? Предъявив такое число n, для которого n * n = 4. И мы знаем это число... )
deniok: (lambda cube)
Коллеги! Не будет ли слишком изощренным издевательством во вводной части обзора Агды, при самом начале обсуждения типа Vec привести такие примеры
[true,false,true] : Vec Bool 3
[2,12,85,0,6] : Vec ℕ 5
Поясню - я не хочу в этом месте вдаваться в детали описания конструкторов, а скрытый здесь грандиозный обман я честным образом раскрою позже.
deniok: (ухмыляюсь)
Что-то у меня хаскелевский импорт вот так работает
{-# IMPORT System.IO #-}
а вот так ломается
{-# IMPORT System.IO (hPutStrLn) #-}
говоря Parse error (hPutStrLn). Хотя у Норелла в Dependently Typed Programming in Agda список импорта в примере используется. Agda 2.3.0.1 под Windows. Посмотрите у кого более свежая (2.3.2) и/или другая OS.
deniok: (Default)
open import Data.Nat

data Fin : Set where
  fzero : {n : } → Fin (suc n)
  fsuc  : {n : } → Fin n → Fin (suc n)

magic₁ : {A : Set} → Fin zero → A
magic₁ ()

magic₂ : {A : Set} → Fin zero → A
magic₂ n = _
Для того, чтобы правильно сделать коду на Агде грамотную синтаксическую раскраску, требуется не просто полноценно его распарсить, но ещё и повычислять изрядно по ходу дела. То есть ждать приличных внешних тулзов нечего, хочешь цветной Агды - сиди в emacs и не жужжи.

Между тем, хотелось бы (из педагогических, к примеру, соображений) иметь хорошо раскрашенный агдо-код для вставки куда угодно, и не в виде картинки. Отсюда вопрос - нельзя ли вытащить информацию о раскраске из emacs'а?

Я никому не скажу, что я большую часть времени работаю в Windows, поэтому мой вопрос относится в основном к этой OS, но если, например, это очень легко в какой другой OS, а в богомерзкой - очень сложно, то это была бы тоже полезная информация.

UPD1. Как нам сообщают умные люди в комментах можно:
(1) использовать саму Агду, она умеет генерировать правильно размеченный html:
agda --html --html-dir=<куда выводить> <корневой модуль>
(2) в emacs можно использовать htmlize (или htmlfontify, но у первого, вроде, настройки побогаче).

UPD2. Поправил цвета на в точности стандартные, а то некоторые ругаются.
deniok: (Default)
Оказывается, абсурдный образец не обязателен (хотя и часто полезен) при отсутствии допустимых образцов конструктора:
module AbsurdTest where

data   False : Set where -- необитаемый
record True  : Set where -- синглетон

data Bool : Set where
  true  : Bool
  false : Bool

-- декодирующая функция для булева универсума
isTrue : Bool → Set
isTrue true  = True
isTrue false = False

not_ : Bool → Bool
not true  = false
not false = true

-- абсурдистская версия
lem-not²≡id₁ : (a : Bool) → isTrue (not not a) → isTrue a
lem-not²≡id₁ true p = p
lem-not²≡id₁ false ()

-- обывательская версия
lem-not²≡id₂ : (a : Bool) → isTrue (not not a) → isTrue a
lem-not²≡id₂ true  p = p
lem-not²≡id₂ false p = p
Во второй версии во втором клозе мы спокойно пишем p, хотя его тип isTrue (not not false) редуцируется к необитаемому False.

С каноническим примером такое не пройдёт
open import Data.Nat

data Fin : ℕ → Set where
  fzero : {n : ℕ} → Fin (suc n)
  fsuc  : {n : ℕ} → Fin n → Fin (suc n)

magic₁ : {A : Set} → Fin zero → A
magic₁ ()

magic₂ : {A : Set} → Fin zero → A
magic₂ n = {! !}
Если здесь в дырку в magic₂ засунуть _, то нам покрасят его жёлтым, сигнализируя тем самым, что подходящей метапеременной Агде тут не вывести.
deniok: (Default)
на почве русской Википедии. Вот плод:

http://ru.wikipedia.org/wiki/Agda

Улучшайте при желании, не ухудшайте без особой нужды.
deniok: (lambda cube)
Напоминаю, что очередная встреча SPbHUG, которую теперь зовут FProg, пройдёт в четверг, 12 июля в 19:00 в офисе компании Яндекс. Предполагается, что нашему вниманию будут предложены следующие доклады:
  • Jan Malakhovski Введение в Agda.
  • Evgeny Kotelnikov Зависимые типы в Haskell.
  • Andrey Vlasovskikh Команда spb-archlinux на ICFP Contest 2009.

Подробная информация и регистрация на странице встречи.

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Syndicate

RSS Atom

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 25th, 2017 02:53 pm
Powered by Dreamwidth Studios