How do I give a type for this code?

Haskell community, I'm in one of those situations where I have the code I want to write, but need to find the right types to get it to typecheck. What follows is a generic version of my situation. Suppose I want to represent the finite models of a language (in the sense of mathematical logic) with a single constant c, unary function symbol f, and predicate P. I can represent the carrier as a list m, the constant as an element of m, the function as a list of ordered pairs of elements of m, and the predicate as the list of the elements in the model that satisfy it: -- a model is (m, c, f, p) type Model a = ([a], a, [(a,a)], [a]) -- a is the "base type" I can then construct particular models and operations on models. The details aren't important for my question, just the types: unitModel :: Model () unitModel = ([()], (), [((),())], []) cycleModel :: Int -> Model Int cycleModel n = ([0..n-1], 0, [(i, (i+1)`mod`n) | i<-[0..n-1]], [0]) -- function application, assuming function is total ap :: Eq a => [(a,b)] -> a -> b ap ((x',y'):ps) x = if x == x' then y' else ap ps x -- 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 powerModel :: (Eq a, Ord a) => Model a -> Model [a] powerModel (m, c, f, p) = (ms, cs, fs, ps) where ms = subsequences m cs = [c] fs = [(xs, nub (sort (map (ap f) xs))) | xs <- ms] ps = [xs | xs <- ms, elem c xs] Now, I want to give a name to all of these models: data ModName = UnitModel | CycleModel Int | Product ModName ModName | Power ModName deriving (Show, Eq) And finally, I want to associate each name with its associated model: 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) I've tried a number of ways of getting this to work, in the sense of defining types so that I can use exactly this definition of model_of (some involving GADTs and type families) but haven't found a best way. How should I do it? Todd Wilson

Hi Todd, the problem is, that 'model_of' tries to return different types: Model a, Model (a,a) and Model [a]. I think you have to use some kind of ADT also for the Model, like you already did for ModName. Something like: data Model a = Model a | ProductModel (a,a) | PowerModel [a] ... Greetings, Daniel
participants (2)
-
Daniel Trstenjak
-
Todd Wilson