HList 친절하지 승격

Question

내가 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은 홍보 할 수 없습니다 종류? GHC 7.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 : 주된 목표는 온실 가스를 추정하는 것입니다.

(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에 납득시킬 수있는 또 다른 방법이 있습니까?

Answer 1

이제 질문은 (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) 

하지만 하스켈 따라 유형이 없습니다. "속이는"의존형은 일반적으로 유형이 존재한다는 증거를 가지고있는 증인을 갖는 것을 의미합니다. 이것은 다소 지루한 일이지만, 현재 다른 방법은 없습니다. 우리는 이미 목록 xs에 대한 증인을 가지고 있습니다 - 정확히 HList xs입니다.

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

그래서 우리 형이된다 :

는

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

함수의 몸은 아주 간단 제약을 위해, 우리는 그 다음 우리는 간단한 함수로 의미를 작성할 수

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

를 사용합니다 - 의 각 패턴이 :++:의 정의에서 각 패턴과 일치하는 방식에 유의하십시오.

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)입니다. 사실 함수 정의는 동일합니다.