9

我试图回答我自己关于在 GHC 中使用 PolyKinds 扩展的示例的问题，并提出了一个更具体的问题。我正在尝试对一个由两个列表构建的队列进行建模，头列表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)
4

1 回答 1

5

按照 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.
于 2011-12-30T08:14:37.957 回答