Wie kann ich dieses abhängig typisierte Beispiel in Haskell codieren?

Question

Angenommen, ich möchte die endlichen Modelle der Sprache erster Ordnung mit der Konstante c, unäre Funktion Symbol f und Prädikat P darstellen. Ich kann den Träger als Liste m, die Konstante als ein Element von m, die Funktion als darstellen eine Liste von geordneten Paaren von Elementen der m (die über eine Hilfsfunktion ap angewendet werden kann), und das Prädikat als eine Liste der Elemente der m die es erfüllen:

-- Models (m, c, f, p) with element type a 
type Model a = ([a], a, [(a,a)], [a]) 

-- helper function application, assumes function is total 
ap :: Eq a => [(a,b)] -> a -> b 
ap ((x',y'):ps) x = if x == x' then y' else ap ps x 

I kann dann bestimmte Modelle bauen und Operationen an Modellen. Die Details sind nicht wichtig für meine Frage, nur die Typen (aber ich habe die Definitionen enthalten, damit Sie sehen können, wo die Typeinschränkungen kommen aus):

unitModel :: Model() 
unitModel = ([()],(), [((),())], []) 

cyclicModel :: Int -> Model Int 
cyclicModel n | n > 0 = ([0..n-1], 0, [(i, (i+1)`mod`n) | i<-[0..n-1]], [0]) 

-- cartesian product of models 
productModel :: (Eq a, Eq b) => Model a -> Model b -> Model (a,b) 
productModel (m1, c1, f1, p1) (m2, c2, f2, p2) = (m12, c12, f12, p12) where 
    m12 = [(x1,x2) | x1 <- m1, x2 <- m2] 
    c12 = (c1, c2) 
    f12 = [(x12, (ap f1 (fst x12), ap f2 (snd x12))) | x12 <- m12] 
    p12 = [x12 | x12 <- m12, elem (fst x12) p1 && elem (snd x12) p2] 

-- powerset of model (using operations from Data.List) 
powerModel :: (Eq a, Ord a) => Model a -> Model [a] 
powerModel (m, c, f, p) = (ms, cs, fs, ps) where 
    ms = subsequences (sort m) -- all subsets are "normalized" 
    cs = [c] 
    fs = [(xs, nub (sort (map (ap f) xs))) | xs <- ms] -- "renormalize" the image of f 
    ps = [xs | xs <- ms, elem c xs] 

Nun, ich möchte Namen geben, um alle diese Modelle:

data ModelName = UnitModel 
       | CyclicModel Int 
       | Product ModelName ModelName 
       | Power ModelName 
       deriving (Show, Eq) 

Schließlich möchte ich diesen Code schreiben, jeden Namen Zuordnung zum Modell es Namen:

model_of UnitModel = unitModel 
model_of (CycleModel n) = cycleModel n 
model_of (Product m1 m2) = productModel (model_of m1) (model_of m2) 
model_of (Power m1) = powerModel (model_of m1) 

ich eine Reihe von Ansätzen zu machen dies zu arbeiten versucht haben, in der Sinn der Definition von ty pes, so dass ich genau diese Definition von model_of verwenden kann, einschließlich der Verwendung von Phantom-Typen, GADTs und Typfamilien - habe aber keinen Weg gefunden, dies zu tun. (Aber andererseits bin ich ein relativer Neuling in Haskell.) Kann es getan werden? Wie soll ich das machen?

Answer 1

Mit einem GADT für ModelName können Sie einen bestimmten Namen mit dem Typparameter des resultierenden Modells verknüpfen. Hier ist, was gebraucht wird, um Ihre model_of Kompilierung zu machen:

{-# LANGUAGE GADTs #-} 

data ModelName t where 
    UnitModel :: ModelName() 
    CyclicModel :: Int -> ModelName Int 
    Product  :: (Eq a, Eq b) => ModelName a -> ModelName b -> ModelName (a, b) 
    Power  :: (Ord a) => ModelName a -> ModelName [a] 

model_of :: ModelName t -> Model t 
model_of UnitModel  = unitModel 
model_of (CyclicModel n) = cyclicModel n 
model_of (Product m1 m2) = productModel (model_of m1) (model_of m2) 
model_of (Power m1)  = powerModel (model_of m1) 

EDIT: wie Sie vielleicht bemerkt, die normale deriving Klausel funktioniert nicht mit GADTs aber es stellt sich heraus StandaloneDeriving funktioniert gut.

{-# LANGUAGE StandaloneDeriving #-} 

deriving instance Show (ModelName t) 
deriving instance Eq (ModelName t) 

Beachten Sie jedoch, dass die Eq Instanz in diesem Fall ein bisschen unsinnig ist, weil die Typ-Klasse ermöglicht es Ihnen, nur die Werte des gleichen Typs zu vergleichen, aber die unterschiedlichen Hersteller im Wesentlichen produzieren Werte verschiedenen Typen. So zum Beispiel, wird die folgende nicht einmal Typprüfung:

UnitModel == CyclicModel 

weil UnitModel und CyclicModel verschiedene Typen haben (ModelName() und ModelName Int respectively). Für Situationen, in denen Sie die zusätzliche Typ-Informationen aus irgendeinem Grunde löschen Sie einen Wrapper wie

data Some t where 
    Some :: t a -> Some t 

verwenden können, und Sie können zum Beispiel ableiten eine Eq Instanz für Some ModelName manuell:

{-# LANGUAGE FlexibleInstances #-} 

instance Eq (Some ModelName) where 
    Some UnitModel == Some UnitModel 
     = True 

    Some (CyclicModel n) == Some (CyclicModel n') 
     = n == n' 

    Some (Product m1 m2) == Some (Product m1' m2') 
     = Some m1 == Some m1' && Some m2 == Some m2' 

    Some (Power m1) == Some (Power m1') 
     = Some m1 == Some m1' 

    _ == _ = False