How do I code this dependently-typed example in Haskell?

Question

Suppose I want to represent the finite models of the first-order language with 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 (which can be applied via a helper function ap), and the predicate as a list of the elements of m that satisfy it:

-- 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 can then construct particular models and operations on models. The details aren't important for my question, just the types (but I've included the definitions so you can see where the type constraints come from):

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]

Now, I want to give names to all of these models:

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

Finally, I want to write this code, mapping each name to the model it names:

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 approaches to making this to work, in the sense of defining types so that I can use exactly this definition of model_of, including using phantom types, GADTs, and type families -- but haven't found a way to do it. (But then again, I'm a relative newcomer to Haskell.) Can it be done? How should I do it?

shang shang · Accepted Answer · 2013-10-18T05:13:48

By using a GADT for ModelName you can associate a given name with the resulting model's type parameter. Here's what's needed to make your model_of compile:

{-# 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: as you noticed, the normal deriving clause doesn't work with GADTs but it turns out StandaloneDeriving works just fine.

{-# LANGUAGE StandaloneDeriving #-}

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

Note, however, that the Eq instance is a bit nonsensical in this case because the type-class allows you to only compare values of the same type, but the different constructors essentially produce values of different types. So, for example, the following does not even type-check:

UnitModel == CyclicModel

because UnitModel and CyclicModel have different types (ModelName () and ModelName Int respectively). For situations where you need to erase the additional type-information for some reason you can use a wrapper such as

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

and you can derive e.g. an Eq instance for Some ModelName manually:

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

How do I code this dependently-typed example in Haskell?

1 Answers