haskell에 종속 유형화 된 큐

Question

examples using the PolyKinds extension in GHC에 대한 내 자신의 질문에 답하려고 시도하고보다 구체적인 문제가 발생했습니다. 나는 두 개의리스트, 즉 dequeue이 요소를 취하는 head-list와 enqueue이 붙이는 tail-list로 구성된 큐를 모델링하려고한다. 이 흥미로운 부분을 만들기 위해 필자는 꼬리표가 헤드 목록보다 길어질 수 없다는 제약 조건을 추가하기로했습니다.

큐가 균형을 유지해야하는 경우 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

다음 피그 워커 (pigworker)가 다음과 같은 코드를 작성했습니다. 큐를 제약 조건에 다시 설정해야하고 적절한 버전의 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.