LINUX.ORG.RU

Равные длины векторов


0

0

Навеяно вялотекущей дискуссией про зависимые типы.

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

Нам хочется, чтобы компилятор гарантировал нам, что длины этих векторов одинаковы. Чтобы если мы где-то наглючили и породили вектора разной длины, программа не скомпилировалась бы.

Пример того, как подобные вещи могут делаться в Хаскеле:

module Test where
data Nil = Nil
data Cons a = Cons Integer a
class ScalarProduct a where scalarProduct :: a -> a -> Integer
instance ScalarProduct Nil where scalarProduct Nil Nil = 0
instance ScalarProduct a => ScalarProduct (Cons a) where scalarProduct (Cons n1 a1) (Cons n2 a2) = n1 * n2 + scalarProduct a1 a2
main :: Integer -> Integer
main n = main' n 0 Nil Nil where
  main' :: ScalarProduct a => Integer -> Integer -> a -> a -> Integer
  main' 0 _ as bs = scalarProduct as bs
  main' n i as bs = main' (n-1) (i+1) (Cons (2*i+1) as) (Cons (i^2) bs)
Здесь, получается, ТИП списка содержит в некотором роде его ДЛИНУ, то есть списки разной длины будут разных типов, списки одной длины - одного типа.

Я попытался воспроизвести то же самое в плюсах, используя шаблоны вместо Cons и main'. Наткнулся на бесконечное разворачивание шаблонов. Товарищи плюсисты, как делаются подобные вещи?

★★★★★
Ответ на: комментарий от Miguel

> Если мы при компиляции не знаем

А кто эти самые «мы» — «мы, люди» или «мы и компилятор»? Даст ли компилятор нам при необходимости выстрелить в ногу, и как в таких случаях штатными средствами сказать компилятору «все будет хорошо, мамой клянусь»?

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

Ну, не о том, чтобы ВСЁ... То есть, там всё плохо, но речь только о кусочке.

Какие из приведенных примеров будут компилироваться, какие — нет, и как компилятор это определяет?

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

main1 m n = main1p m n Nil Nil
   where
      main1p 0 0 a b = ScalarProduct a b
      main1p i 0 a b = main1p (i-1) 0 (Cons i a) b
      main1p 0 j a b = main1p 0 (j-1) a (Cons j b)
      main1p i j a b = main1p (i-1) (j-1) (Cons i a) (Cons j b)
то компилироваться опять не будет, второе из уравнений в определении main1p требует, чтобы a и Cons i a были одного типа - что означает, что компилятор будет жаловаться на рекурсивный тип. Рекурсивные типы возможны, но должны быть явными.

Второй пример компилироваться не будет, там у функции сons нет конкретного типа. Что она возвращает? Nil? Cons Nil? Cons (Cons Nil)?

Третий пример компилироваться не будет по той же причине.

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

Даст ли компилятор нам при необходимости выстрелить в ногу, и как в таких случаях штатными средствами сказать компилятору «все будет хорошо, мамой клянусь»?

Это и есть unsafe-функции. Cкажем, функция unsafeCoerce имеет тип a -> b для любых a и b. Если вы уверены, что a и b ВСЕГДА будут равными, то вы можете её использовать; она ведёт себя как id. Но если вы ошибётесь - произойдёт что угодно.

Можно также задать instance Typeable для наших типов (обычно его можно просто сдерайвить). Тогда вы можете использовать функцию coerce :: (Typeable a, Typeable b) => a -> Maybe b. Она даст вам Just, если типы совпадают, и Nothing, если нет. Такая вот рантаймовая проверка, основанная на рефлекшене. Эта функция уже совершенно безопасна. Но тогда, например, в типе функции main' будет также ограничение Typeable a - что как бы намекает, что автор функции не справился с системой типов.

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