3

大量の GHC 拡張機能を使用するこのコード スニペットがあります。

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import GHC.Exts (Constraint)

data HList :: [*] -> * where
    Nil  :: HList '[]
    Cons :: a -> HList l -> HList (a ': l)

type family All (p :: * -> Constraint) (xs :: HList [*]) :: Constraint where
    All p Nil = ()
    All p (Cons x xs) = (p x, All p xs)

GHC は次のように訴えています。

 ‘HList’ of kind ‘[*] -> *’ is not promotable
    In the kind ‘HList [*]’

HList種類を昇格できないのはなぜですか? GHC7.8.2とを使用しても同じエラーが発生します7.11。

もちろん、ビルトインを使用しても'[]問題なく動作します。

type family All (p :: * -> Constraint) (xs :: [*]) :: Constraint where
    All p '[]       = ()
    All p (x ': xs) = (p x, All p xs)

実際には追加がサポートされており、次のようになっているため、HList代わりに自分のものを使用したいと思います。'[]HList

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

data HList :: [*] -> * where
    Nil  :: HList '[]
    Cons :: a -> HList l -> HList (a ': l)
    App  :: Hlist a -> HList b -> HList (a :++: b)

EDIT：主な目標は、GHCに推論させることです

(All p xs, All p ys) ==> All p (xs :++: ys)

書けるように

data Dict :: Constraint -> * where
    Dict :: c => Dict c

witness :: Dict (All p xs) -> Dict (All p ys) -> Dict (All p (xs :++: ys))
witness Dict Dict = Dict

型レベルのリストを追加するための明示的な表現を追加することが、これを達成するのに役立つことを願っていました。GHCに上記のことを納得させる別の方法はありますか?

4

1 に答える 1

5

問題は の証明をどのように書くかであることがわかりました(All p xs, All p ys) => All p (xs :++: ys)。もちろん、答えは帰納法によるものです！

本当に書きたい関数の型は

allAppend :: (p :: Constraint) -> (xs :: [*]) -> (ys :: [*]) 
          -> (All p xs, All p ys) -> All p (xs :++: ys)

Haskell には依存型がありません。依存型の「偽装」とは、通常、型が存在するという証拠を保持する証人を持つことを意味します。これはやや面倒ですが、現在のところ他に方法はありません。私たちはすでにリストの証人を持っていますxs- それはまさにHList xs. 制約には、使用します

data Dict p where Dict :: p => Dict p

次に、含意を単純な関数として記述できます。

type (==>) a b = Dict a -> Dict b

したがって、私たちのタイプは次のようになります。

allAppend :: Proxy p -> HList xs -> HList ys 
          -> (All p xs, All p ys) ==> (All p (xs :++: ys))

関数の本体は非常に単純です。allAppendの各パターンが の定義の各パターンとどのように一致するかに注目して:++:ください。

allAppend _ Nil _  Dict = Dict  
allAppend _ _  Nil Dict = Dict 
allAppend p (Cons _ xs) ys@(Cons _ _) Dict = 
  case allAppend p xs ys Dict of Dict -> Dict

反対の含意All p (xs :++: ys) => (All p xs, All p ys)も成り立ちます。実際、関数の定義は同じです。

于 2015-01-19T14:14:34.580 に答える