2011-12-29 9 views
9

Ho provato a rispondere alla mia domanda su examples using the PolyKinds extension in GHC e ho trovato un problema più concreto. Sto provando a modellare una coda che è composta da due elenchi, l'elenco di testa da cui prende gli elementi da dequeue e l'elenco di coda dove li posiziona lo enqueue. Per rendere questo interessante, ho deciso di aggiungere un vincolo che la coda non può essere più lunga dell'elenco principale.Coda Dipendentemente digitata in haskell

Sembra che enqueue debba restituire tipi diversi se la coda deve essere bilanciata o meno. E 'possibile dare un tipo corretto per la funzione enqueue con questo vincolo?

Il codice che ho attualmente è qui:

{-#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` 

Le liste di livello di tipo ausiliarie e nats sono definiti di seguito.

-- 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) 
+3

Chiedetevi che cosa si desidera che il tipo di code per dirvi. Vuoi mantenere l'invariante (tra le liste) internamente? Vuoi esporre la lunghezza della coda? Puoi anche considerare di archiviare il testimone alla differenza nelle lunghezze delle liste, che diminuiranno fino a zero quando accodati, indicando facilmente quale politica scegliere e quando riequilibrare. – pigworker

risposta

5

Seguendo i suggerimenti di Pigworkers sono riuscito a inserire il seguente bit di codice. Ho aggiunto un flag per il quale la coda deve essere ripristinata al vincolo e utilizzata per inviare la chiamata alla versione corretta di enqueue.

Il risultato è un po 'prolisso e sto ancora cercando risposte o miglioramenti migliori su questo. (io non sono nemmeno sicuro che realmente sono riuscito a coprire tutti i casi di rottura invarianti con i vincoli.)

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