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