คิวที่พิมพ์ขึ้นอยู่กับ haskell

ฉันพยายามตอบคำถามของตัวเองเกี่ยวกับ ตัวอย่างที่ใช้ส่วนขยาย PolyKinds ใน GHC และมา กับปัญหาที่เป็นรูปธรรมมากขึ้น ฉันกำลังพยายามสร้างโมเดลคิวที่สร้างจากสองรายการ ได้แก่ head-list ที่ dequeue รับองค์ประกอบมา และ tail-list ที่ 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)

types haskell dependent-type
person aleator    schedule 29.12.2011    source แหล่งที่มา
comment
ถามตัวเองว่าคุณต้องการให้ประเภทของ Queue บอกอะไรคุณ คุณต้องการรักษาค่าคงที่ (ระหว่างรายการ) ภายในหรือไม่? คุณต้องการเปิดเผยความยาวของคิวหรือไม่? คุณอาจต้องการพิจารณาจัดเก็บพยานตามความยาวรายการที่แตกต่างกัน ซึ่งจะลดลงเหลือศูนย์เมื่อคุณเข้าคิว เพื่อบอกคุณอย่างง่ายดายว่าควรเลือกนโยบายใดและเมื่อใดควรปรับสมดุล   -  person pigworker    schedule 29.12.2011

คำตอบ (1)


arrow_upward
5
arrow_downward

การติดตาม 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.
person aleator    schedule 30.12.2011