Неявные аргументы и семейства типов

Я экспериментировал с программами с зависимой типизацией, используя библиотеку Data.Singletons, после разработки векторов с аннотациями длины в статье «Зависимо типизированное программирование с синглетонами» и столкнулся со следующей проблемой.

Этот код, за исключением определения функции indexI, проверяет типы в GHC 7.6.3 и работает, как ожидалось, в его отсутствие:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Singletons
import Data.Singletons.TH

data Nat where
  Z :: Nat
  S :: Nat -> Nat
  deriving Eq

$(genSingletons [''Nat])

data FlipList :: * -> * -> Nat -> * where
    Cons :: ((a -> b) -> a -> b) -> FlipList a (a -> b) n -> FlipList a b (S n)
    Nil :: FlipList a b Z

type family (m :: Nat) :< (n :: Nat) :: Bool
type instance m :< Z = 'False
type instance Z :< (S n) = 'True
type instance (S m) :< (S n) = m :< n

type family PreMap a b (m :: Nat) :: *
type instance PreMap a b Z = a -> b
type instance PreMap a b (S n) = PreMap a (a -> b) n

type family BiPreMap a b (m :: Nat) :: *
type instance BiPreMap a b m = PreMap a b m -> PreMap a b m

index :: ((m :< n) ~ 'True) => SNat m -> FlipList a b n -> BiPreMap a b m
index SZ (Cons f _) = f
index (SS sm) (Cons _ fl) = index sm fl

indexI :: ((m :< n) ~ 'True, SingI m) => FlipList a b n -> BiPreMap a b m
indexI = withSing index

После включения indexI GHC выдает две ошибки:

Could not deduce (PreMap a b m ~ PreMap a b a0)
    from the context ((m :< n) ~ 'True, SingI Nat m)
      bound by the type signature for
                 indexI :: ((m :< n) ~ 'True, SingI Nat m) =>
                           FlipList a b n -> BiPreMap a b m

а также,

Could not deduce (PreMap a b m ~ PreMap a b a0)
    from the context ((m :< n) ~ 'True, SingI Nat m)
      bound by the type signature for
                 indexI :: ((m :< n) ~ 'True, SingI Nat m) =>
                           FlipList a b n -> BiPreMap a b m

Причина любой ошибки, по-видимому, в том, что термин withSing index имеет тип FlipList a b n -> BiPreMap a b a0, и, не имея возможности вывести a0 ~ m, GHC не может доказать BiPreMap a b m ~ BiPreMap a b a0. Я знаю, что в выводе типов по семействам типов не хватает большинства удобств, которые мы получаем при работе с ADTS (инъективность, генеративность и т. Д.), Но мое понимание того, в чем именно заключается проблема в этом случае и как ее обойти, очень ограничено. . Могу ли я указать какое-то ограничение, которое может прояснить это?


types singleton haskell gadt
person Mark    schedule 25.05.2014    source источник
comment
У меня работает следующее: indexI :: forall m n a b . ((m :< n) ~ 'True, SingI m) => FlipList a b n -> BiPreMap a b m; indexI = withSing (index :: SNat m -> FlipList a b n -> BiPreMap a b m)   -  person user2407038    schedule 26.05.2014

Ответы (1)


arrow_upward
2
arrow_downward

Здесь вы должны понимать, что в вашем коде нет ничего плохого, просто вывод типа GHC не может определить, насколько он безопасен. Обратите внимание, что, закомментировав indexI, загрузив код в GHC и запросив тип withSing index:

*Main Data.Singletons> :t withSing index
  withSing index
    :: (SingI Nat a, (a :< n) ~ 'True) =>
       FlipList a1 b n -> PreMap a1 b a -> PreMap a1 b a

Это означает, что GHC может проверить тип вашего кода и даже вывести тот же тип, что и указанный вами (с точностью до альфа-эквивалентности). Так почему же он не проверяет тип вашего кода?

Проблема в том, что в вашем коде явно не указано, как должны быть созданы экземпляры параметров типа withSing, в частности, переменная типа a должна быть создана для m из вашей сигнатуры типа. Вполне возможно, что a должен быть создан для чего-то еще (например, [m] или m -> m), чтобы ваша реализация withSing index имела указанный вами тип. GHC не может определить, что a должен быть создан для m, вы получите ошибки, которые получите. Обратите внимание, что GHC не будет пытаться угадать такого рода экземпляры, и это хорошо. Мы не хотим, чтобы язык уровня типов GHC выродился в интерпретатор Пролога;). На мой взгляд, это уже слишком близко к этому.

Это означает, что у вас есть два варианта решения вашей проблемы. Первое решение было предложено пользователем2407038 выше: используйте аннотации типов, чтобы сообщить GHC, как должен быть создан экземпляр параметра типа a функции withSing. Позвольте мне повторить его код здесь для справки:

indexI :: forall m n a b . ((m :< n) ~ 'True, SingI m) => FlipList a b n -> BiPreMap a b m
indexI = withSing (index :: SNat m -> FlipList a b n -> BiPreMap a b m)

Обратите внимание, что вам нужен явный синтаксис forall в сигнатуре типа, чтобы убедиться, что m из сигнатуры типа находится в области видимости реализации indexI (дополнительную информацию см. В документации по расширению GHC ScopedTypeVariables).

Другой альтернативой является изменение кода, чтобы GHC мог определить, как создать экземпляр a по выводу типа. Чтобы понять это, представьте, что GHC сообщает вам, что не может вывести PreMap a b m ~ PreMap a b a0. Это означает, что GHC сделал вывод withSing index на тип, который я показал вам в начале этого ответа, и пытается найти экземпляры типов, чтобы определить, насколько этот предполагаемый тип равен типу, который вы аннотировали. Для этого он пытается решить ограничение равенства BiPreMap a b m ~ BiPreMap a b a0, которое упрощено до более простого ограничения PreMap a b m ~ PreMap a b a0. Однако здесь он застревает. Поскольку семейства типов, такие как PreMap, не обязательно являются инъективными, из этого нельзя решить, что m должно быть равно a0. Один из способов решить эту проблему - изменить BiPreMap на тип данных или новый тип. В отличие от семейств типов, типы данных и новые типы являются инъективными в своих аргументах, и GHC может разрешить ограничения:

newtype BiPreMap a b m = BiPreMap { getBiPreMap :: PreMap a b m -> PreMap a b m }

index :: ((m :< n) ~ 'True) => SNat m -> FlipList a b n -> BiPreMap a b m
index SZ (Cons f _) = BiPreMap f
index (SS sm) (Cons _ fl) = BiPreMap (getBiPreMap (index sm fl))

indexI :: ((m :< n) ~ 'True, SingI m) => FlipList a b n -> BiPreMap a b m
indexI = withSing index

Вот и все, я надеюсь, что это проясняет кое-что из того, что происходит ... Обратите внимание, что тип «программирования с зависимой типизацией в Haskell», который вы пытаетесь реализовать, нетривиален в Haskell, и вы можете столкнуться с другими подобными проблем по пути. Очень часто явные сигнатуры типов будут решением для странных ошибок типа, с которыми вы можете столкнуться. Также были бы полезны приложения с явным типом, но я понимаю, что их поддержка в GHC все еще отсутствует или выполняется.

person Dominique Devriese    schedule 26.05.2014