kouzdra: А вообще по первому впечатлению AGDA забавно, но не то, что мне хотелось:

А вообще по первому впечатлению AGDA забавно, но не то, что мне хотелось:
Заинтересовался я наличием там типа List⁺ - но был разочарован:

Он оказался просто парой:

List⁺ : ∀ {a} → Set a → Set a
List⁺ A = A × List A

Что можно и на Haskell спокойной написать - и даже посредством классов типов сделать "safe" специализацией List.

А я надеялся, что там можно как-то на уровне типовой системы накладывать допограничения на уже имеющийся тип, так чтобы List⁺ был разновидностю List, но такой, что на уровне типов зашито, что он ≠ []

Хотя все равно язычок интересный, да и то, что наконец-то кто-то догадался использовать матзначки из unicode в синтаксисе - порадовало. Сколько можно.

(Добавить комментарий)

	qwerty 2014-09-13 14:18 (ссылка)
	Юникодные матзначки использовались еще в Фортрэссе. (Ответить)

	tomcatkins 2014-09-13 19:20 (ссылка)
	надо все значки из апла в юникод воткнуть (Ответить) (Ветвь дискуссии)

	в анус себе воткни, пес (Анонимно) 2014-09-13 20:58 (ссылка)
	The Unicode Basic Multilingual Plane includes the APL symbols in the Miscellaneous Technical block, which are therefore usually rendered accurately from the larger Unicode fonts installed with most modern operating systems. (Ответить) (Уровень выше)

zhd
2014-09-17 12:36 (ссылка)

Рано разочаровались. Делается это так. Задается индуктивное семейство списков, знающих свою длину (более известные как векторы):

data Vec (X : Set) : Nat -> Set where
[] : Vec X 0
_::_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)

Непустой список это просто Vec X (suc n), а, скажем, Vec X (suc (suc n)) -- это список где есть точно два элемента.

Можно, например, написать безопасную функцию, возвращающею первый элемент:
head : {X : Set}{n : Nat} -> Vec X (suc n) -> X
head (x :: xs) = x
Процедура унификации видит, что индекс (suc n) нельзя унифицировать с нулем, поэтому кейс [] можно не писать.

Но самое интересное начнется, когда у функции несколько аргументов и они связаны через индекс. Рассмотрим тип конечных множеств:
data Fin : Nat -> Set where
fz : {n : Nat} -> Fin (suc n)
fs : {n : Nat} -> Fin n -> Fin (suc n)

Его можно использовать для получения произвольного элемента списка:
lookup : {X : Set}{n : Nat} -> Fin n -> Vec X n -> X
lookup fz (x :: xs) = x
lookup (fs i) (x :: xs) = lookup i xs
Опять же из-за унификации индексов случаи, когда требуется получить элемент с номером за границей массива, полностью исключены. В этом сила зависимых типов.

Разумеется можно следить за огромным количеством свойств, но не всегда ясно как сделать элегантно. Одним из ведущих спецов поэтому вопросу является Конор МакБрайд, см. его недавнюю работу ``How to keep your neighbors in order'', где он разбирает случаи структур, которые можно сортировать, причем делает это политипически, т.е. сразу для немаленького универсума типов. То о чем мечтали фантасты, натурально.

(Ответить)

zhd
2014-09-17 12:48 (ссылка)

Есть альтернативный путь накладывания ограничений. Пусть у нас имеется обычный тип списков List и функция длины length : {X : Set} -> List X -> Nat. Тогда можем определить тип:
Vec : (X : Set)(n : Nat) -> Set
Vec X n = Sg (List X) (\ x -> length x == n)
, где Sg -- зависимая сумма.

Т.е. теперь вектор, это просто пара, состоящая из обычного списка и доказательства, что его длина равна n.

Есть интересная статья про что если функция, фигурирующая в равенстве является примитивно-рекурсивной, то описание типа можно представить виде индуктивного семейства.

(Ответить)