Есть ли способ открыть словари ограничений во время компиляции в GHC?

Question

Рассмотрим следующий код на Haskell (GHC 8.2):

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Constraint

type family Head xs where
  Head (x ': xs) = x

type family Tail xs where
  Tail (x ': xs) = xs

class IsList xs where
  isList :: (xs ~ '[] => r) -> ((xs ~ (Head xs ': Tail xs), IsList (Tail xs)) => r) -> r

instance IsList '[] where isList r _ = r
instance IsList xs => IsList (x ': xs) where isList _ r = r

type family Prepend xs ys where
  Prepend '[] ys = ys
  Prepend (x ': xs) ys = x ': Prepend xs ys

prependPreservesIsList :: forall xs ys. (IsList xs, IsList ys) => Dict (IsList (Prepend xs ys))
prependPreservesIsList = isList @xs Dict (withDict (prependPreservesIsList @(Tail xs) @ys) Dict)

class IsList (Deps a) => Hard (a :: *) where
  type Deps a :: [*]

instance (Hard a, Hard b) => Hard (Either a b) where
  type Deps (Either a b) = Prepend (Deps a) (Deps b)

с ошибкой

Main.hs:37:10: error:
    • Could not deduce (IsList (Prepend (Deps a) (Deps b)))
        arising from the superclasses of an instance declaration
      from the context: (Hard a, Hard b)
        bound by the instance declaration at Main.hs:37:10-46
    • In the instance declaration for ‘Hard (Either a b)’
   |
37 | instance (Hard a, Hard b) => Hard (Either a b) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Код пытается создать класс Hard, который имеетсвязанный список типов Deps, где Deps, соответствующий Either a b, должен быть объединением Deps, соответствующим a и b.

Мы знаем, какдоказать GHC, что эта форма объединения сохраняет класс IsList, о чем свидетельствует prependPreservesIsList.Если бы у нас было (Hard a, Hard b), и нам нужно было написать нормальный код, который требовал бы (IsList (Deps (Either a b))), мы бы просто withDict prependPreservesIsList и были бы в пути.Но нам нужно, чтобы GHC распознал это ограничение «во время компиляции», чтобы обеспечить допустимость экземпляра Either a b.

Есть ли способ «открыть словарь ограничений» во время компиляции илив противном случае отменить этот код, чтобы GHC принял экземпляр Either a b?

Answer 1

Рассмотрите возможность перехода от списков уровня типов к деревьям уровня типов.Итак:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

data Tree a = Empty | Node a | Branch (Tree a) (Tree a)

class IsTree xs where
    isTree ::
        (xs ~ 'Empty => a) ->
        (forall x. xs ~ 'Node x => a) ->
        (forall l r. (xs ~ 'Branch l r, IsTree l, IsTree r) => a) ->
        a

instance IsTree 'Empty where isTree a _ _ = a
instance IsTree ('Node x) where isTree _ a _ = a
instance (IsTree l, IsTree r) => IsTree ('Branch l r) where isTree _ _ a = a

class IsTree (Deps a) => Hard a where
    type Deps a :: Tree *

instance (Hard a, Hard b) => Hard (Either a b) where
    type Deps (Either a b) = 'Branch (Deps a) (Deps b)

Answer 2

Существует еще один способ представления ограничений класса типов в виде словарей первого класса (Dict), хотя он и не так эргономичен:

class Hard a where
  type Deps a :: [*]
  depsIsList :: Dict (IsList (Deps a))

instance (Hard a, Hard b) => Hard (Either a b) where
  type Deps (Either a b) = Prepend (Deps a) (Deps b)
  depsIsList =
   case depsIsList @a of
     Dict ->
       case depsIsList @b of
         Dict -> prependPreservesIsList @(Deps a) @(Deps b)

Использование (:-) из ограничений пакет может сделать составление таких словарей чуть менее болезненным.