Как правильно обернуть тип данных, индексируемый индуктивным типом данных? - PullRequest
Новая
       26

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

1 голос
/ 26 октября 2019

Я пытаюсь тонко обернуть одну версию списка. У меня проблемы с деконструкцией. Вот минимальная реализация: 

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ExplicitForAll #-}

module InductiveWrapper where

import Data.Kind (Type)
import Data.Proxy (Proxy)

import GHC.Prim (coerce)

data List a = Nil | Cons a (List a)

data SList :: [ k ] -> Type where
  SNil  ::                        SList '[]
  SCons :: Proxy k -> SList ks -> SList (k ': ks)

newtype Set a = S [ a ]

data SSet :: Set k -> Type where
  SS :: SList xs -> SSet ('S xs)

type family Add (el :: k) (set :: Set k) :: Set k where
  Add el ('S xs) = 'S (el ': xs)

uncons :: forall k (el :: k) (set :: Set k)
        . SSet (Add el set) -> (Proxy el, SSet set)
uncons (SS (x `SCons` xs)) = (x, SS xs)

Вот соответствующий бит ошибки: 

Could not deduce: set ~ 'S ks
      from the context: Add el set ~ 'S xs
        bound by a pattern with constructor:
                   SS :: forall k (xs :: [k]). SList xs -> SSet ('S xs),
                 in an equation for ‘uncons’
[...]
 or from: xs ~ (k1 : ks)
        bound by a pattern with constructor:
                   SCons :: forall k1 (k2 :: k1) (ks :: [k1]).
                            Proxy k2 -> SList ks -> SList (k2 : ks),
[...]
• Relevant bindings include
        xs :: SList ks (bound at InductiveWrapper.hs:37:29)
        x :: Proxy k1 (bound at InductiveWrapper.hs:37:19)
        xs' :: SList xs (bound at InductiveWrapper.hs:37:14)
        s :: SSet (Add el set) (bound at InductiveWrapper.hs:37:8)

Проблема, как я понимаю, состоит в том, что Add el set застревает, потому что средство проверки типа неПонимаете, что единственный способ создать set - это использовать 'S.

Как мне снять его или решить эту проблему другими способами? Помимо использования type вместо newtype. Вся причина, по которой я это делаю, заключается в том, чтобы полностью скрыть использование [ k ] и SList.

1 Ответ

2 голосов
/ 26 октября 2019

Семейства типов не являются инъективными, что технически означает, что вы не можете переходить от результата к аргументам справа налево. Кроме нет. В GHC 8.0 введена TypeFamilyDependencies, которая позволяет вам указывать инъективность для семейств типов, например: 

type family Add (el :: k) (set :: Set k) = (set' :: Set k) | set' -> el set where
  Add el ('S xs) = 'S (el ': xs)

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

Но у меня действительно есть другой обходной путь: вы можете отказаться от всей проблемы с инъекцией и указать свой тип семейства другойнаоборот - из списка в кортеж. За исключением того, что вам понадобятся два семейства типов - одно для головы и одно для хвоста: 

type family Head set where Head ('S (el ': xs)) = el
type family Tail set where Tail ('S (el ': xs)) = 'S xs

uncons :: SSet set -> (Proxy (Head set), SSet (Tail set))
uncons (SS (x `SCons` xs)) = (x, SS xs)

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

class Uncons set res | set -> res  where
    uncons :: SSet set -> res

instance Uncons ('S (el ': xs)) (Proxy el, SSet ('S xs)) where
    uncons (SS (x `SCons` xs)) = (x, SS xs)
...