Невозможно преобразовать список уровня типа обратно в уровень значения с помощью библиотеки синглетонов - PullRequest
1 голос
/ 02 июля 2019

Я пытаюсь написать s разумно статически проверенную систему авторизации [1], и в настоящее время пытаюсь написать функцию, которая извлечет необходимые разрешения из аннотации / фантома на уровне типа дляуровень значения.

{-# LANGUAGE DataKinds, GADTs, ScopedTypeVariables #-}

module Try5 where

import Control.Monad.Reader
import Data.Singletons
import Data.Singletons.TH


data Permission = PermA
                | PermB
                deriving (Eq, Show)
$(genSingletons [''Permission])

data Env = Env

newtype AppM (perms :: [Permission]) a = AppM (ReaderT Env IO a) deriving (Functor, Applicative, Monad, MonadIO, MonadReader Env)

-- other functions for constructing an action in `AppM perms`
-- have been removed for brevity

runAction :: AppM (perms :: [Permission]) () -> IO ()
runAction _ = do
  let permissions :: [Permission] = fromSing $ singByProxy (Proxy :: Proxy (perms :: [Permission]))
  putStrLn $ "Huzzah, I freed the permissions from the type-level cage: " <> (show permissions)
  pure ()

Ошибка:

    • Ambiguous type variable ‘a0’ arising from a use of ‘singByProxy’
      prevents the constraint ‘(SingI a0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘a0’ should be.
      These potential instances exist:
        instance forall a (n1 :: a) (n2 :: [a]).
                 (SingI n1, SingI n2) =>
                 SingI (n1 : n2)
          -- Defined in ‘singletons-2.4.1:Data.Singletons.Prelude.Instances’
        instance SingI '[]
          -- Defined in ‘singletons-2.4.1:Data.Singletons.Prelude.Instances’
    • In the second argument of ‘($)’, namely
        ‘singByProxy (Proxy :: Proxy (perms :: [Permission]))’
      In the expression:
        fromSing $ singByProxy (Proxy :: Proxy (perms :: [Permission]))
      In a pattern binding:
        permissions :: [Permission]
          = fromSing $ singByProxy (Proxy :: Proxy (perms :: [Permission]))
   |
24 |   let permissions :: [Permission] = fromSing $ singByProxy (Proxy :: Proxy (perms :: [Permission]))
   |                                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[1] Больше контекста можно найти на https://stackoverflow.com/a/56828016/534481

1 Ответ

3 голосов
/ 02 июля 2019

perms не входит в область действия runAction. Он должен быть явно связан с forall. См. документ на ScopedTypeVariables.

Другая проблема состоит в том, что для «понижения» значения из типов требуется экземпляр SingI.

Ключевая интуиция заключается в том, что forall вводит нерелевантные переменные времени выполнения: если runAction :: forall p. ... не имеет никаких ограничений, runAction @p не может фактически зависеть от значения p, оно всегда должно делать то же самое , Тезис Ричарда Айзенберга, Зависимые типы в Хаскеле: теория и практика , содержит более подробную информацию по этому вопросу (раздел 4.2).

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

runAction :: forall perms. SingI perms => AppM perms () -> IO ()
...