タイプレベルリストを '[]のためのセンチネルのないネストされたタプルに分解する

Question

タイプのリスト（例えば'[Int, Int]）を型とその型を作成するための方法の両方に解体しようとしています（ネストされたタプルと同形ですが、より良い書き込みをする）。例：

{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TypeInType #-} 
{-# LANGUAGE TypeFamilies, FlexibleInstances #-} 

import Data.Kind (Type) 

data a :<> b = a :<> b 
infixr 8 :<> 

class Construct a where 
    type Result a :: Type 

instance forall a as. (Show a, Construct as) => Construct (a:as) where 
    type Result (a:as) = a :<> (Result as) 

instance Construct '[] where 
    type Result '[] =() 

これを使用すると、

λ :kind! Result '[Int, Int, Int] 
Result '[Int, Int, Int] :: * 
= Int :<> (Int :<> (Int :<>())) 

最後に私がしたくないのは:<>()です。最初はリストエレメントの長さに合わせてより具体的にマッチングを試みました。 「[A、B]：

instance forall a b. (Show a, Show b) => Construct ('[a,b]) where 
    type Result '[a,b] = a :<> b 

しかし、動作しませんもちろん：

Conflicting family instance declarations: 
    Result (a : as) = a :<> Result as -- Defined at test.hs:14:8 
    Result '[a, b] = a :<> b -- Defined at test.hs:22:8 

私は常にN特定のインスタンスまで構築することができます。

instance forall a. (Show a) => Construct '[a] where 
    type Result '[a] = a 

instance forall a b. (Show a, Show b) => Construct '[a,b] where 
    type Result '[a, b] = a :<> b 

instance forall a b c. (Show a, Show b, Show c) => Construct '[a,b,c] where 
    type Result '[a, b, c] = a :<> b :<> c 

-- etc. up to N 

しかし、それはそうです非常に満足していない。

再帰的定義を使用してInt :<> (Int :<> (Int :<>())))の代わりにInt :<> (Int :<> Int)に解凍する方法はありますか？

Answer 1

閉じたタイプのファミリを使用します。彼らはトップからボトムまで一致しているので、矛盾はありません。

今

type family Construct (xs :: [Type]) :: Type where 
    Construct '[x]  = x 
    Construct (x ': xs) = x :<> Construct xs 

Construct [Int, Int, Int]Int :<> (Int :<> Int)に減少します。

しかし、あなたがこれをどのように使うのかについて大雑把に言えば、異種のリストを扱うほうがずっと簡単です。型推論の方が簡単です。 HListに便利な操作のための一例として、

{-# language 
    UndecidableInstances, RankNTypes, TypeOperators, TypeFamilies, 
    TypeApplications, ScopedTypeVariables, GADTs, DataKinds, PolyKinds, 
    ConstraintKinds, AllowAmbiguousTypes #-} 

import Data.List 
import Data.Kind 

data HList (ts :: [Type]) :: Type where 
    Nil :: HList '[] 
    (:>) :: t -> HList ts -> HList (t ': ts) 
infixr 5 :> 

-- example 
foo :: HList [Int, String, Bool] 
foo = 0 :> "foo" :> True :> Nil 

、我々は各要素の型は、クラスの制約を満たすことがわかっている場合、我々は、均質なリストにそれを集めるか、要素タイプを保存のいずれか、リストの上にマッピングすることができます。

type family AllC c (xs :: [a]) :: Constraint where 
    AllC c '[]  =() 
    AllC c (x ': xs) = (c x, AllC c xs) 

hmap :: forall c ts. AllC c ts => (forall x. c x => x -> x) -> HList ts -> HList ts 
hmap f Nil  = Nil 
hmap f (x :> xs) = f x :> hmap @c f xs 

hmap' :: forall c ts r. AllC c ts => (forall x. c x => x -> r) -> HList ts -> [r] 
hmap' f Nil  = [] 
hmap' f (x :> xs) = f x : hmap' @c f xs 

TypeApplicationsを使用して、cの制約を設定できます。私たちは、単にhmap'を使用してHListためShowインスタンスを実装することができます

instance AllC Show ts => Show (HList ts) where 
    show xs = "[" ++ intercalate ", " (hmap' @Show show xs) ++ "]" 

今、私たちはGHCiの中に持っている：fooのすべての要素タイプがShowインスタンスを持っているので、作品

> foo 
[0, "foo", True] 

。