haskellの従属型キュー

Question

私はexamples using the PolyKinds extension in GHCについて私自身の質問に答えようとし、より具体的な問題を思いつきました。私は、dequeueが要素を取るヘッドリストとenqueueが置くテールリストの2つのリストから構築されたキューをモデル化しようとしています。 これを興味深くするために、私は、テールリストがヘッドリストより長くなることはできないという制約を加えることにしました。

enqueueは、キューのバランスを取る必要がある場合は、異なるタイプを返す必要があるようです。 この制約でenqueue関数に適切な型を与えることは可能ですか？私は現在持っている

コードはここにある：

{-#LANGUAGE MultiParamTypeClasses, FlexibleInstances, 
    UndecidableInstances, TypeFamilies, PolyKinds, GADTs, 
    RankNTypes#-} 

-- Queue consist of a head and tail lists with the invariant that the 
-- tail list should never grow longer than the head list. 

-- Type for representing the invariant of the queue 
data MyConstraint = Constraint Nat Nat 
type family Valid c :: Bool 
type instance Valid (Constraint a b) = GE a b 

-- The queue type. Should the constraint be here? 
data Queue :: * -> MyConstraint -> * where 
    Empty :: Queue a (Constraint Zero Zero) 
    NonEmpty :: Valid (Constraint n m) ~ True => 
      LenList a n -> LenList a m -> Queue a (Constraint n m) 

instance (Show a) => Show (Queue a c) where 
    show Empty = "Empty" 
    show (NonEmpty a b) = "NonEmpty "++quote a ++ " " ++ quote b 

quote a = "("++show a++")" 

-- Check the head of the queue 
peek :: GE m (Succ Zero) ~ True => Queue a (Constraint m n) -> a 
peek (NonEmpty (CONS a _) _) = a 

-- Add an element to the queue where head is shorter than the tail 
push :: (Valid (Constraint m (Succ n))) ~ True => 
     a -> Queue a (Constraint m n) -> Queue a (Constraint m (Succ n)) 
push x (NonEmpty hd as) = NonEmpty hd (CONS x as) 

-- Create a single element queue 
singleton :: (Valid (Constraint (Succ Zero) Zero)) ~ True => 
     a -> Queue a (Constraint (Succ Zero) Zero) 
singleton x = NonEmpty (CONS x NIL) NIL 

-- Reset the queue by reversing the tail list and appending it to the head list 
reset :: (Valid (Constraint (Plus m n) Zero)) ~ True => 
     Queue a (Constraint m n) -> Queue a (Constraint (Plus m n) Zero) 
reset Empty = Empty 
reset (NonEmpty a b) = NonEmpty (cat a b) NIL -- Should have a reverse here 

enqueue :: ?? 
enqueue = -- If the tail is longer than head, `reset` and then `push`, otherwise just `push` 

補助型レベルリストおよびNATのは以下に定義されています。

-- Type Level natural numbers and operations 

data Nat = Zero | Succ Nat deriving (Eq,Ord,Show) 

type family Plus m n :: Nat 
type instance Plus Zero n = n 
type instance Plus n Zero = n 
type instance Plus (Succ m) n = Succ (Plus m n) 

type family GE m n :: Bool 
type instance GE (Succ m) Zero = True 
type instance GE Zero (Succ m) = False 
type instance GE Zero Zero = True 
type instance GE (Succ m) (Succ n) = GE m n 

type family EQ m n :: Bool 
type instance EQ Zero Zero = True 
type instance EQ Zero (Succ m) = False 
type instance EQ (Succ m) Zero = False 
type instance EQ (Succ m) (Succ n) = EQ m n 

-- Lists with statically typed lengths 
data LenList :: * -> Nat -> * where 
    NIL :: LenList a Zero 
    CONS :: a -> LenList a n -> LenList a (Succ n) 

instance (Show a) => Show (LenList a c) where 
    show x = "LenList " ++ (show . toList $ x) 

-- Convert to ordinary list 
toList :: forall a. forall m. LenList a m -> [a] 
toList NIL = [] 
toList (CONS a b) = a:toList b 

-- Concatenate two lists 
cat :: LenList a n -> LenList a m -> LenList a (Plus n m) 
cat NIL a = a 
cat a NIL = a 
cat (CONS a b) cs = CONS a (cat b cs) 

Answer 1

次のように、私は次のコードを書きとめました。私は、キューを制約にリセットする必要があるというフラグを追加して、適切なバージョンのenqueueにコールをディスパッチするためにそれを使用しました。

結果は少し冗長ですが、私はまだこれについてより良い回答や改善を探しています。 （私は制約と不変破断例すべてをカバーするために管理していることも、本当にわからない。）

-- Type for representing the invariant of the queue 
data MyConstraint = Constraint Nat Nat Bool 
type family Valid c :: Bool 
type instance Valid (Constraint a b c) = GE a b 

type family MkConstraint m n :: MyConstraint 
type instance MkConstraint m n = Constraint m n (EQ m n) 

-- The queue type. Should the constraint be here? 
data Queue :: * -> MyConstraint -> * where 
    Empty :: Queue a (MkConstraint Zero Zero) 
    NonEmpty :: --Valid (Constraint n m True) ~ True => -- Should I have this here? 
      LenList a n -> LenList a m -> Queue a (MkConstraint n m) 

instance (Show a) => Show (Queue a c) where 
    show Empty = "Empty" 
    show (NonEmpty a b) = "NonEmpty "++quote a ++ " " ++ quote b 

quote a = "("++show a++")" 

-- Check the head of the queue 
peek :: GE m (Succ Zero) ~ True => Queue a (Constraint m n f) -> a 
peek (NonEmpty (CONS a _) _) = a 

-- Since the only way to dispatch using the type seems to be a typeclass, 
-- and enqueue must behave differently with different constraint-types it follows 
-- that the enqueue needs to be in a typeclass? 
class Enqueue a where 
    type Elem a :: * 
    type Next a :: * 
    -- Add an element to the queue where head is shorter than the tail 
    enqueue :: Elem a -> a -> Next a 

-- Enqueuing when the queue doesn't need resetting. 
instance Enqueue (Queue a (Constraint m n False)) where 
    type Elem (Queue a (Constraint m n False)) = a 
    type Next (Queue a (Constraint m n False)) = 
     (Queue a (MkConstraint m (Succ n))) 
    enqueue x (NonEmpty hd as) = NonEmpty hd (CONS x as) 

-- Enqueuing when the queue needs to be reset. 
instance Enqueue (Queue a (Constraint m n True)) where 
    type Elem (Queue a (Constraint m n True)) = a 
    type Next (Queue a (Constraint m n True)) = 
     Queue a (MkConstraint (Plus m (Succ n)) Zero) 
    enqueue x Empty = NonEmpty (CONS x NIL) NIL 
    enqueue x (NonEmpty hd tl) = NonEmpty (cat hd (CONS x tl)) NIL 
        -- Should have a reverse tl here. Omitted for 
        -- brevity.