haskell中的依賴類型隊列

Question

我試圖回答我自己關於examples using the PolyKinds extension in GHC的問題，並提出了一個更具體的問題。我試圖建立一個從兩個列表構成的隊列，dequeue從中獲取元素的頭部列表以及enqueue放置它們的尾部列表。 爲了使這個有趣，我決定添加一個約束條件，尾列表不能長於頭列表。

看起來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

以下pigworkers提示我設法湊齊了下面的代碼。我添加了一個標誌，表明隊列需要重置爲約束條件，並用它來調用正確版本的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.