haskell - 有没有办法在 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实例？

标签： haskellghc

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)