[Haskell-beginners] How do I give a type for this code?
Todd Wilson
twilson at csufresno.edu
Tue Oct 15 22:11:22 UTC 2013
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20131015/2aa4d89c/attachment.html>
More information about the Beginners
mailing list