другой ответ очень умный (пожалуйста, найдите время, чтобы проголосовать за него), но как человек, не знакомый с Agda, как это будет реализован на Haskell, для меня не было очевидным. Вот полная версия Haskell. Нам понадобится множество расширений, а также Data.Type.Equality
(поскольку нам нужно будет выполнить некоторое ограниченное количество проверок типов).
{-# LANGUAGE GADTs, ScopedTypeVariables,RankNTypes,
TypeInType, TypeFamilies, TypeOperators #-}
import Data.Type.Equality
Определение Nat
, Vec
и Queue
Затем мы определяем обычные натуральные числа на уровне типа (это выглядит как обычное определение data
, но поскольку у нас включено TypeInType
, оно будет автоматически повышаться, когда мы используем его в типе) и функцию типа (type family
) для добавление. Обратите внимание, что хотя существует несколько способов определения +
, наш выбор здесь повлияет на то, что будет дальше. Мы также определим обычный Vec
, который очень похож на список, за исключением того, что он кодирует свою длину в фантомном типе n
. С этим мы можем пойти дальше и определить тип нашей очереди.
data Nat = Z | S Nat
type family n + m where
Z + m = m
S n + m = S (n + m)
data Vec a n where
Nil :: Vec a Z
(:::) :: a -> Vec a n -> Vec a (S n)
data Queue a where
Queue :: { front :: Vec a (n + m)
, rear :: Vec a m
, schedule :: Vec x n } -> Queue a
Определение rotate
Теперь все начинает становиться более волосатым. Мы хотим определить функцию rotate
, имеющую тип rotate :: Vec a n -> Vec a (S n + m) -> Vec a m -> Vec a (S n + m)
, но вы быстро столкнетесь с множеством проблем, связанных с доказательствами, просто определяя ее рекурсивно. Решение состоит в том, чтобы вместо этого определить немного более общий grotate
, который может быть определен рекурсивно, и для которого rotate
является частным случаем.
Смысл Bump
в том, чтобы обойти тот факт, что в Haskell нет такой вещи, как композиция на уровне типов. Невозможно записать такие операторы, как (∘)
, чтобы (S ∘ S) x
было S (S x)
. Обходной путь заключается в постоянном переносе/развертывании с помощью Bump
/lower
.
newtype Bump p n = Bump { lower :: p (S n) }
grotate :: forall p n m a.
(forall n. a -> p n -> p (S n)) ->
Vec a n ->
Vec a (S n + m) ->
p m ->
p (S n + m)
grotate cons Nil (y ::: _) zs = cons y zs
grotate cons (x ::: xs) (y ::: ys) zs = lower (grotate consS xs ys (Bump (cons y zs)))
where
consS :: forall n. a -> Bump p n -> Bump p (S n)
consS = \a -> Bump . cons a . lower
rotate :: Vec a n -> Vec a (S n + m) -> Vec a m -> Vec a (S n + m)
rotate = grotate (:::)
Здесь нам нужны явные forall
, чтобы было ясно, какие переменные типа захватываются, а какие нет, а также для обозначения типов более высокого ранга.
Одноэлементные натуральные числа SNat
Прежде чем мы перейдем к exec
, мы настроим некоторый механизм, который позволит нам доказать некоторые арифметические утверждения на уровне типов (которые нам нужны для того, чтобы exec
выполнил проверку типов). Начнем с создания типа SNat
(который является одноэлементным типом, соответствующим Nat
). SNat
отражает свое значение в переменной фантомного типа.
data SNat n where
SZero :: SNat Z
SSucc :: SNat n -> SNat (S n)
Затем мы можем сделать пару полезных функций для работы с SNat
.
sub1 :: SNat (S n) -> SNat n
sub1 (SSucc x) = x
size :: Vec a n -> SNat n
size Nil = SZero
size (_ ::: xs) = SSucc (size xs)
Наконец, мы готовы доказать некоторую арифметику, а именно, что n + S m ~ S (n + m)
и n + Z ~ n
.
plusSucc :: (SNat n) -> (SNat m) -> (n + S m) :~: S (n + m)
plusSucc SZero _ = Refl
plusSucc (SSucc n) m = gcastWith (plusSucc n m) Refl
plusZero :: SNat n -> (n + Z) :~: n
plusZero SZero = Refl
plusZero (SSucc n) = gcastWith (plusZero n) Refl
Определение exec
Теперь, когда у нас есть rotate
, мы можем определить exec
. Это определение выглядит почти так же, как и в вопросе (со списками), за исключением аннотации gcastWith <some-proof>
.
exec :: Vec a (n + m) -> Vec a (S m) -> Vec a n -> Queue a
exec f r (_ ::: s) = gcastWith (plusSucc (size s) (sub1 (size r))) $ Queue f r s
exec f r Nil = gcastWith (plusZero (sub1 (size r))) $
let f' = rotate f r Nil in (Queue f' Nil f')
Вероятно, стоит отметить, что мы можем получить кое-что бесплатно, используя singletons
. С включенными правильными расширениями следующий более читаемый код
import Data.Singletons.TH
singletons [d|
data Nat = Z | S Nat
(+) :: Nat -> Nat -> Nat
Z + n = n
S m + n = S (m + n)
|]
определяет Nat
, семейство типов :+
(эквивалентное моему +
) и одноэлементный тип SNat
(с конструкторами SZ
и SS
эквивалентными моим SZero
и SSucc
) все в одном.
person
Alec
schedule
26.10.2016
exec
иrotate
с векторной реализацией? - person user2407038   schedule 14.04.2016forall x . { ... ; schedule :: Vec sl x }
? Мне кажется, чтоschedule
по существу является натуральным числом, потому что единственное, что вы знаете о нем, — это его длина, поскольку его содержание экзистенциально квантифицировано. Таким образом, типschedule
, вероятно, должен бытьSing sl
. - person user3237465   schedule 14.04.2016schedule
действительно представляет натуральное число (и я ввелx
специально, чтобы убедиться, что оно используется только как натуральное число), но на самом деле это часть переднего списка, поэтому сопоставление с образцом для него управляет инкрементным вычислением этого списка. - person dfeuer   schedule 14.04.2016exec
может быть выражен по-разному, в зависимости от того, что работает лучше всего, но я считаю, что одним допустимым выражением являетсяVec (sl1 :+ rl) a -> Vec rl a -> Vec ('S sl1) a -> Queue a
- person dfeuer   schedule 14.04.2016