हैकेल

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` 

सहायक प्रकार स्तर सूचियों और Nats नीचे परिभाषित कर रहे हैं।

-- 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.