Как я могу выразить тип «takeWhile for vectors»?

Question

Haskell начинающий здесь. Я определил следующие типы:

data Nat = Z | S Nat 
data Vector a n where 
    Nil :: Vector a Z 
    (:-) :: a -> Vector a n -> Vector a (S n) 
infixl 5 :- 

Я пытаюсь написать функцию, которая ведет себя takeWhileVector такой же, как TakeWhile делает в списках, но на векторах.

Моя реализация выглядит следующим образом:

takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m 
takeWhileVector f Nil = Nil 
takeWhileVector f (x :- xs) = if (f x) then (x :- takeWhileVector f xs) else Nil 

Это не компилируется и выдает следующее сообщение об ошибке:

Could not deduce (m ~ 'S n0) 
from the context (n ~ 'S n1) 
    bound by a pattern with constructor 
      :- :: forall a (n :: Nat). a -> Vector a n -> Vector a ('S n), 
      in an equation for ‘takeWhileVector’ 
    at takeWhileVector.hs:69:20-26 
    ‘m’ is a rigid type variable bound by 
     the type signature for 
     takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m 
     at takeWhileVector.hs:67:20 
Expected type: Vector a m 
    Actual type: Vector a ('S n0) 
Relevant bindings include 
    takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m 
    (bound at takeWhileVector.hs:69:1) 
In the expression: (x :- takeWhileVector f xs) 
In an equation for ‘takeWhileVector’: 
    takeWhileVector f (x :- xs) = (x :- takeWhileVector f xs) 

я бы подумал, что мое определение типа для takeWhileVector говорит следующее:

Для всех типов «a» и «n» типа Nat эта функция возвращает «Вектор a m», где «m» - вид Nat.

Нужно ли менять подпись типа takeWhileVector более конкретно, чтобы он показывал, что результатом является вектор a (m :: Nat)? В противном случае, как я могу изменить это, чтобы оно скомпилировалось?

Answer 1

типа вы предлагаете не может быть реализован, то есть он не заселен:

takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m 

Помните, что абонент выбирает переменные типа a,n,m. Это означает, что вызывающий может использовать вашу функцию, например.

takeWhileVector :: (a -> Bool) -> Vector a Z -> Vector a (S Z) 

который нонсенс, так как вы не можете произвести некоторые a сек, если вы не получили ни в самом начале. Более того, вызывающий объект этой функции не может выбрать, сколько результатов будет иметь и передать полностью несвязанную функцию, - которая не согласуется с предполагаемой семантикой takeWhile.

Я предполагаю, что вы на самом деле означает что-то вроде

takeWhileVector :: (a -> Bool) -> Vector a n -> exists m. Vector a m 

за исключением того, что exists не действует синтаксис Haskell. Вместо этого вам нужно что-то вроде

data SomeVector a where 
    S :: Vector a m -> SomeVector a 

takeWhileVector :: (a -> Bool) -> Vector a n -> SomeVector a 

Answer 2

Там нет никакого способа, чтобы статический знать длину Vec, возвращенные takeWhileVec: она зависит от значений, содержащихся в Vec и функции, которую вы используете. Однако, что я могу сделать, это дать вам значение, которое вы можете сопоставить с образцом на . Изучите длину Vec. Введите singleton values.

data Natty n where 
    Zy :: Natty Z -- pronounced 'zeddy', because I'm a limey 
    Sy :: Natty n -> Natty (S n) -- pronounced 'essy' 

Для данного n в своем роде Nat, существует ровно один (не undefined) значение типа Natty n. Так что если вы знаете что-то о Natty, вы знаете что-то о связанной с ним уровне типа Nat. *

Почему мы не можем просто использовать Nat для этой цели? Haskell поддерживает разделение между значениями и типами.Уровень типа Nat не имеет никакого отношения, кроме структурного сходства, к значению уровня Nat: значение S Z имеет тип Nat, а не S' Z' - поэтому мы должны использовать Natty, вторую копию Nat, чтобы вручную связать значений и типов вместе. (Real-типизированных в зависимости системы, такие как Agda позволяют повторно использовать тот же Nat для обоих значений уровня и вычислений типа уровня.)

_{* Вы можете распространять знания другим способом тоже, используя классы типов.}

---

План состоит в том, чтобы вернуть выходной вектор, а также ее длину, как Natty, с типами, расположенных таким образом, что GHC понимает, что Natty действительно представляет его длину. Вы могли бы сначала рассмотреть этот вариант на примере в вашем вопросе:

-- takeWhile :: (a -> Bool) -> Vec a n -> (Natty m, Vec a m) 

Но это не говорит, правильно: мы говорим takeWhile может вернуть любой m выбора вызывающего абонента, который не так! Он может возвращать только уникальный m, определенный функцией и входным вектором. Как я уже упоминал, это невозможно узнать во время компиляции, поэтому мы должны держать длину в секрете от компилятора.

data AVec a = forall n. AVec (Natty n) (Vec a n) 

AVec является existential type: n появляется на правой стороне, но не слева. Этот метод позволяет эмулировать dependent pair type: тип Vec зависит от значения Natty. Зависимые пары полезны, когда статические свойства данных зависят от динамической информации, недоступной во время компиляции.

Мы можем написать takeWhile прямолинейно Сейчас:

takeWhile :: (a -> Bool) -> Vec a n -> AVec a 
takeWhile f Nil = AVec Zy Nil 
takeWhile f (x :- xs) = case takeWhile f xs of 
          AVec n ys -> if f x 
              then AVec (Sy n) (x :- ys) 
              else AVec Zy Nil 

Мы должны были выбросить статическое знание длины вектора, так как вы используете AVec с функцией, которая ставит статические требования по длине? Из-за пути AVec мы знаем, что Natty в левом слоте представляет длину вектора в правом слоте: оба они имеют одинаковый (экзистенциально скрытый) параметр типа n. Итак, по шаблону соответствия на Natty, мы узнаем длину Vec.

head :: Vec a (S n) -> a 
head (x :- xs) = x 

head' :: AVec a -> Maybe a 
head' (AVec Zy Nil) = Nothing 
head' (AVec (Sy n) xs) = Just (head xs) 

В этом примере мы только заботиться, является ли вектор больше, чем один, так что шаблон согласования на Sy достаточно, чтобы доказать GHC, что мы должны быть позволено использовать head. (См a related answer of mine для более сложного примера доказательства фактов о AVec с.)

---

@chi упоминается дразнящая идея: вы можете показать, что вектор возвращаемого takeWhile не длиннее входного вектора.

takeWhile :: (a -> Bool) -> Vec a n -> AShorterVec a n 

, где AShorterVec не является тип векторов не больше n. Наша задача - записать определение AShorterVec.

Учитывая два натуральных числа, как вы можете быть уверены, что первое меньше или равно второму? Отношение является индуктивным. Если левый операнд равен нулю, то он будет равен или меньше любому натуральному числу автоматически. В противном случае число меньше или равно другому, если его предшественник меньше или равно другому предшественнику другого. Мы можем кодировать это как конструктивное доказательство с использованием GADT.

data LTE n m where 
    ZLte :: LTE Z m 
    SLte :: LTE n m -> LTE (S n) (S m) 

Если n меньше m, вы сможете придумать значение LTE n m. Если это не так, вы не можете. Вот что такое Curry-Howard isomorphism.

Теперь мы готовы определить AShorterVec: для того, чтобы построить значение AShorterVec a n вы должны быть в состоянии доказать, что он короче, чем n путем подачи значения LTE m n. Когда вы сопоставляете шаблон с конструктором AShorterVec, он дает вам доказательство, чтобы вы могли его вычислить.

data AShorterVec a n = forall m. AShorterVec (LTE m n) (Vec a m) 

takeWhile составляет лишь незначительные изменения: мы должны управлять этим доказательством объекта.

takeWhile :: (a -> Bool) -> Vec a n -> AShorterVec a n 
takeWhile f Nil = AShorterVec ZLte Nil 
takeWhile f (x :- xs) = case takeWhile f xs of 
          AShorterVec prf ys -> if f x 
                then AShorterVec (SLte prf) (x :- ys) 
                else AShorterVec ZLte Nil 

---

Альтернативный способ дать тип для takeWhile, чтобы подтолкнуть верхнюю грань по длине в самом тип возвращаемого, а не носить его вокруг как данные. Этот подход не распространяется на любые споры с Natty, такие как LTE и экзистенциальные количественные оценки. не

data ShorterVec a n where 
    SNil :: ShorterVec a n 
    SCons :: a -> ShorterVec a n -> ShorterVec a (S n) 

Еще раз, ShorterVec a n обозначает множество векторов не больше n. Структура ShorterVec напоминает finite sets, но переведена из мира естественных в мир векторов. Пустой вектор короче любой длины, которую вы хотите назвать; ячейка cons увеличивает наименьшую допустимую верхнюю границу на одну. Обратите внимание, что значение n никогда полностью не определяется значением типа ShorterVec, поэтому вы можете присвоить действительную верхнюю границу ShorterVec. Эти два выражения как хорошо напечатал:

ok1 = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S (S (S Z))) 
ok2 = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S (S Z)) 

но это один не является:

-- notOk = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S Z) -- the vector is longer than our stated upper bound. 

Используя этот тип данных, вы можете написать красиво простую версию takeWhile, которая выглядит точно так же, как в оригинальной версии списка :

takeWhile :: (a -> Bool) -> Vec a n -> ShorterVec a n 
takeWhile f Nil = SNil 
takeWhile f (x :- xs) = if f x 
         then SCons x (takeWhile f xs) 
         else SNil 

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

toAVec :: ShorterVec a n -> AVec a 
toAVec SNil = AVec Zy Nil 
toAVec (SCons x xs) = case toAVec xs of 
          AVec n ys -> AVec (Sy n) (x :- ys) 

---

Мы начали с помощью одиночек, чтобы связать типы и значение вместе, и экзистенциальные типы завернуть выполнения информации о данных с самими данными.Затем, следуя идее @ chi, мы закодировали (одну часть) правильность из takeWhile в подпись типа с использованием доказательств. Затем мы придумали способ испечь инвариант длины непосредственно к типу возврата, отказавшись от необходимости доказывать любые теоремы.

После того, как у вас есть вкус программируемого на вашем языке программирования, трудно вернуться к старому. Системы выраженного типа дают вам как минимум три преимущества: вы можете писать действующие программы, которые запрещают другие языки (или принудительно дублировать код); вы можете писать более значимые типы для одних и тех же функций, делая более сильные обещания; и вы можете доказать правильность своих программ машинным способом.

Haskell не настроен для этого. Одна из проблем заключается в том, что синглтоны делают ненужным сложность типов привязки и значений: различие вызывает разрыв кода шаблонов, большинство из которых я вас пощадил, чтобы перетасовать между типами и значениями. (Большая часть этого шаблона может быть автоматизирована - вот что дает the singletons library.) Если бы мы хотели указать другой аспект правильности takeWhile - тот факт, что все элементы выходного списка удовлетворяют предикату - нам придется работать исключительно с списки синглетонов и функции предиката типа уровня. Я также считаю утомительным объявлять новый тип верхнего уровня каждый раз, когда я хочу количественно определить что-то экзистенциально (вы можете писать библиотеки, чтобы помочь с этим, хотя они часто приводят к другому шаблону) - у нас есть отсутствие ямбдов на уровне типа Благодарю за это. Другой основной трудностью является ограничение того, что можно повысить до уровня уровня с помощью DataKinds: нельзя продвигать GADT и экзистенциальные типы, поэтому, например, вы не можете иметь многомерный массив, форма которого выражается статически как Vec Nat n , Никакая реальная система, зависящая от типизации, делает зависимые типы такими трудными в использовании!