Зависимо типизированная очередь в haskell

Я попытался ответить на свой вопрос о примерах, использующих расширение PolyKinds в 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)

types haskell dependent-type
person aleator    schedule 29.12.2011    source источник
comment
Спросите себя, что вы хотите, чтобы тип очередей сказал вам. Вы хотите поддерживать инвариант (между списками) внутри? Вы хотите выставить длину очереди? Вы также можете рассмотреть возможность хранения свидетеля разницы в длине списков, которая будет уменьшаться до нуля по мере постановки в очередь, что поможет вам легко определить, какую политику выбрать и когда перебалансировать.   -  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