LINUX.ORG.RU

Вышел пятый выпуск Haskell Platform

 , , , ,


2

5

Вчера, 3 июня, спустя примерно полгода со времени предыдущего релиза, вышел пятый (за номером 2012.2.0.0) выпуск Haskell Platform — простого в установке окружения разработки для языка Haskell.

Данный выпуск включает в себя:

>>> Подробности

★★★★

Проверено: mono ()
Последнее исправление: Silent (всего исправлений: 1)
Ответ на: комментарий от dmfd

Можно же при желании понаписать функций вроде

Можно делать монадические обобщения вроде

headM :: Monad m => [a] -> m a
headM [] = fail "empty list"
headM x = return $ head x

-- > runIdentity (headM [])
-- *** Exception: empty list
-- > headM [] :: Maybe a
-- Nothing

divM :: (Monad m, Integral a) => a -> a -> m a
divM _ 0 = fail "division by zero"
dviM x y = return $ div x y

-- > runIdentity (1 `divM` 0)
-- *** Exception: division by zero
-- > 1 `divM` 0 :: Maybe Int
-- Nothing

readM :: (Monad m, Read a) => String -> m a
readM s | [x] <- [x | (x, "") <- reads s] = return x
        | otherwise = fail $ "parse error: \"" ++ s ++ "\""

-- > runIdentity (readM "q1" :: Identity Int)
-- *** Exception: parse error: "q1"
-- > readM "q1" :: Maybe Int
-- Nothing

которые частичны в одних монадах и тотальны в других.

Как в этом случае будет выглядеть тот же div или head?

Всё может выглядеть точно также (только лучше там где начинаются всякие заморочки с типами), разница в том, что частичная или нетерминируемая функция это нонсенс в агде и не будет пропущена тайпчекером - обычный head просто не пишется. Правильный head для списков это

take : ∀ {a} {A : Set a} → ℕ → List A → List A
take zero    xs       = []
take (suc n) []       = []
take (suc n) (x ∷ xs) = x ∷ take n xs

head : ∀ {a} {A : Set a} → List A → List A
head = take 1

обычный (как в хаскеле) и при этом правильный head возможен для «векторов»:

head : ∀ {a n} {A : Set a} → Vec A (1 + n) → A
head (x ∷ xs) = x

тут на уровне системы типов известно, что в векторе достаточно элементов для выполнения head.

quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto

не будет пропущена тайпчекером - обычный head просто не пишется

Ясно, спасибо.

dmfd
()
Ответ на: комментарий от dmfd

В compile time нельзя проверить, что один из параметров - ноль.

Можно, например, гарантировать проверку делителя на 0 :)

tailgunner ★★★★★
()
Ответ на: комментарий от dmfd

А что возвращать-то в таком случае?

Исключение бросай, например. Хотя это уже не важно - то, что в некотором участке кода не будет division-by-zero, гарантировано.

tailgunner ★★★★★
()
Ответ на: комментарий от dmfd

А что будет с div в агде?

Учитывая, что числа там реализуются как

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

... но допустим, что

postulate
  ℕ : Set
  zero : ℕ
  suc : ℕ → ℕ
  -- etc.

и они реализованы очень хорошо. div из стандартной библиотеки имеет сигнатуру

_div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ

то есть принимает два натуральных числа (то есть термы типа ℕ) и возвращает натуральное число (так что является простой функцией), кроме этого он принимает неявный (implicit) аргумент тип которого зависит (dependent type) от терма divisor, этот неявный аргумент представляет собой доказательство утверждения которое вычисляется в ⊥ если равенство (equality предикат / identity type) divisor ≡ 0 выводимо (decidable) и в ⊤ в обратном случае. То есть тут эта проблема тоже решается на уровне типов, как и в случае с head (только более муторно). Если у нас будет ⊥, ненаселённый тип, то div будет подобен такой функции

foo : ℕ → ℕ → ⊥ → ℕ
foo _ _ = ⊥-elim

её применение foo 1 2 имеет тип ⊥ → ℕ и вычисляется в ⊥-elim, нет доказательства которое можно передать, так что оно не имеет нормальной формы для полного применения и не пройдёт тайпчек.

В случае ⊤ (населённый тип) будет подобно

bar : ℕ → ℕ → ⊤ → ℕ
bar _ _ tt = 42

применение bar 1 2 tt имеет нормальную форму 42 и tt это передаваемое доказательство. В случае с div, так как аргумент неявный, доказательство строится автоматически, tt подставляется неявно. 1 div 1 имеет нормальную форму 1, 1 div 0 не имеет нормальной формы, останавливается на

1 div 0
| (1 divMod 0
   | _.dm 1 0 1
     (λ y y<x →
        _.dm 1 0 y
        (.Induction.WellFounded.Some.wfRec-builder
         (λ dividend →
            (divisor : ℕ) →
            {.Data.Bool.T (.Data.Bool.not ⌊ Nat._≟_ divisor 0 ⌋)} →
            DivMod' dividend divisor)
         (_.dm 1 0) y (<-well-founded′ 1 y y<x)))
     0)

и не проходит тайпчек. Нужно ещё иметь в виду, что dividend и divisor могут не быть термами в канонической форме, а иметь сложную структуру, так что автоматическое построение доказательства может быть не возможно и его нужно будет передать явно.

Интересно ещё, что делать с числами из IO - то ли для них div не применим потому что нельзя построить соответсвующее доказательство, то ли можно как-то выкрутиться.

quasimoto ★★★★
() автор топика
Ответ на: комментарий от quasimoto

Мало что понял :( Но правильно ли я полагаю, что фразу

доказательство строится автоматически, tt подставляется неявно

вкупе с

Интересно ещё, что делать с числами из IO - то ли для них div не применим потому что нельзя построить соответсвующее доказательство,

можно с какой-то натяжкой интерпретировать, как если в compile time вычисляется значение знаменателя? Или возможна какая-то другая (на уровне типов) проверка того, может ли он быть равен нулю? (Не сводится ли второе к первому?)

dmfd
()
Ответ на: комментарий от dmfd

можно с какой-то натяжкой интерпретировать, как если в compile time вычисляется значение знаменателя

Нет, это не значит, что знаменатель вычисляется в compile time, для него просто в compile time доказывается неравенство нулю. Это, буквально, proof carrying code.

Для примера:

t : ℕ → ℕ → ℕ
t m n = m div n

t принимает любые натуральные числа, но div хочет построить доказательство невыводимости n ≡ 0, чего в контексте t сделать нельзя - будет примерно такое сообщение:

Unsolved metas: T (not ⌊ n ≟ 0 ⌋)

так что div применим только тогда когда из контекста выводимо неравенство нулю знаменателя, каких-то знаний чему именно он равен (главное, что не нуль, по сути, просто по всюду поддерживается ℕ \ {0} для нужного аргумента) не предполагается. Такой контекст должен поддерживаться на всём протяжении вызовов div <- t1 <- t2 <- ... и так далее до интерфейса с пользователем, например, до emacs-mode agdы, или до IO (когда agda компилируется в хаскель). При этом интерфейс отделяет консистентное ядро от неконсистентного окружения, IO, например, реализуется как примитивы FFI, поэтому вполне может (и должно) падать, зависать, фильтровать поступающий контент и т.п. По сути, хорошее IO и система событий вообще это такая система, которая будет уметь «добывать» из событий то что можно отдать консистентному ядру и отсеивать остальное.

Касательно постулатов (в т.ч. примитивов FFI), они могут ломать консистентность как добавляя плохие аксиомы, например:

postulate
  contradiction : {ℓ : Level} {φ : Set ℓ} → ¬ φ

absurd : ⊥
absurd = contradiction tt

так и строя FFI к плохим функциям:

postulate
  _div_ : Integer → Integer → Integer

{-# COMPILED _div_ Prelude.div #-}
quasimoto ★★★★
() автор топика
Ответ на: комментарий от dmfd

p.s. мораль: есть язык, код на котором принципиально не падает в рантайме, но этот код как правило нельзя скомпилировать.

dmfd
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.