Индукция на уровне типа в KnownNats: перекрывающиеся экземпляры - PullRequest
Новая
       88

Индукция на уровне типа в KnownNats: перекрывающиеся экземпляры

2 голосов
/ 20 февраля 2020

Я пытаюсь понять, как сделать индукцию на уровне типов в KnownNats. Игрушечный пример, суммирующий по размеру векторы из векторного размера : 

{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE TypeFamilies, TypeApplications, TypeOperators #-}
{-# LANGUAGE RankNTypes, DataKinds #-}

module Main where

import GHC.TypeNats
import qualified Data.Vector.Sized as V

class KnownNat d => SumVectorSized d where
  sumVS :: V.Vector d Int -> Int

instance SumVectorSized 0 where
  sumVS _ = 0

instance (SumVectorSized d, KnownNat d', d' ~ (1+d)) => SumVectorSized d' where
  sumVS vec = V.head vec + sumVS (V.tail vec)

main = do
  let Just vec = V.fromList @4 [1..4]
  print $ sumVS vec

При компиляции это выдает ошибку: 

• Overlapping instances for SumVectorSized 0
    arising from a use of ‘sumVS’
  Matching instances:
    instance SumVectorSized 0 -- Defined at src/Main.hs:14:10
    instance (SumVectorSized d, KnownNat d', d' ~ (1 + d)) =>
             SumVectorSized d'
      -- Defined at src/Main.hs:17:10

I think проблема в том, что GH C не знает, что (1 + d) не равно 0 для любого d. Как я могу понять, что экземпляры не перекрываются? Или есть другой способ сделать этот тип индукции?

Ответы [ 2 ]

2 голосов
/ 20 февраля 2020

Я думаю, что проблема в том, что GH C не знает, что (1 + d) не равно 0 для любого d.

Чтобы определить перекрытие, вы смотрите только на право =>. Они перекрываются: 

SumVectorSized 0
SumVectorSized d'

Как мне понять, что экземпляры не перекрываются?

Добавить {-# OVERLAPPING #-} ко второму экземпляру.

Или есть ли другой способ сделать этот тип индукции?

Это один из многих приемов, чтобы смягчить отсутствие зависимых типов в Haskell. Разумное решение - обратиться к зависимо типизированному языку, такому как Idris или Agda, где индукцию можно сформулировать как простую функцию.

Менее радикальной альтернативой является go через одноэлементный тип Peano: 

data NatS (n :: Nat) where
  ZS :: NatS 0
  SS :: (n' ~ (n-1), n ~ (1 + n')) => NatS n' -> NatS n

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

sumVS :: NatS n -> V.Vector n Int -> Int
sumVS ZS _ = 0
sumVS (SS n) v = V.head v + sumVS (V.tail v)
1 голос
/ 21 февраля 2020

Вы можете реализовать сопоставление на KnownNat s следующим образом: 

matchKnownNat :: forall n r. KnownNat n => Proxy# n -> (n ~ 0 => r) -> (forall m. (KnownNat m, n ~ (1 + m)) => Proxy# m -> r) -> r
matchKnownNat n z s = case natVal' n of
    0 | Refl <- (unsafeCoerce Refl :: n :~: 0) -> z
    n | SomeNat (m :: Proxy m) <- someNatVal (n - 1), Refl <- (unsafeCoerce Refl :: n :~: 1 + m) -> s (proxy# @_ @m)

sumVS может быть реализовано в соответствии с этим соответствием. 

sumVS :: forall n. KnownNat n => V.Vector n Int -> Int
sumVS = matchKnownNat (proxy# @_ @n) (\_ -> 0) (\_ vec -> V.head vec + sumVS (V.tail vec))

Обратите внимание, что оно избыточно для требуют KnownNat n и V.Vector n Int. Векторы всех размеров уже знают свой размер: 

sumVS' :: forall n. V.Vector n Int -> Int
sumVS' v = V.knownLength v (sumVS v)
...