haskellimporteithernewtypebinary-decision-diagram

Patternmatching on 'Or' of 2 newtypes in haskell


I am using a decision diagram library within a haskell program. For this i want to declare 2 different (new)types that keeps track of which kind of decision diagram i am dealing with. The library i am using is cudd, and decision diagram base type from there is a DdNode, but my question is only haskell related.

newtype Bdd = ToBdd Cudd.Cudd.DdNode
newtype Zdd = ToZdd Cudd.Cudd.DdNode

Normally i want to discriminate between them when calling functions, but now i want to use a function which does not have to discriminate between the 2 types. i mainly tried to solve this in 3 different ways:

data Dd = ToBdd Bdd | ToZdd Zdd

printDdInfo :: Dd -> IO()
printDdInfo (ToZdd dd) = do
    putStrLn "Hello, zdd!"
    Cudd.Cudd.cuddPrintDdInfo manager dd
printDdInfo (ToBdd dd) = do
    putStrLn "Hello, bdd!"
    Cudd.Cudd.cuddPrintDdInfo manager dd

printDdInfo :: Either Bdd Zdd -> IO()
printDdInfo (ToZdd dd) = do
    putStrLn "Hello, zdd!"
    Cudd.Cudd.cuddPrintDdInfo manager dd
printDdInfo (ToBdd dd) = do
    putStrLn "Hello, bdd!"
    Cudd.Cudd.cuddPrintDdInfo manager dd
    
printDdInfo :: Either Bdd Zdd -> IO()
printDdInfo dd = case dd of
  Zdd dd -> do
    putStrLn "Hello, bdd!"
    Cudd.Cudd.cuddPrintDdInfo manager dd
  Bdd dd -> do
    putStrLn "Hello, bdd!"
    Cudd.Cudd.cuddPrintDdInfo manager dd

All of these methods failed. What is the most elegant way of writing this code? Thanks for your attention.


Solution

  • I haven't dug too deeply into your code, but from your description it sounds like you might be interested in the idea of a phantom type.

    newtype Dd x = ToDd (Cudd.Cudd.DdNode)
    data B
    data Z
    

    Now you can distinguish between Dd B and Dd Z when you want, and work polymorphically with Dd x when you don't care.

    In modern GHC Haskell, if you want to indicate that B and Z are the only tags, you can use the DataKinds and KindSignatures extensions and do it like this:

    newtype Dd (x :: DdTag) = ToDd (Cudd.Cudd.DdNode)
    data DdTag = B | Z
    

    In this context, you'll deal with Dd 'B and Dd 'Z, where the single quote (pronounced "tick") "promotes" the data constructor to the type level.

    To write a function that behaves differently depending on which tag the type has, you'll need a class.

    class Zoop tag where
      zoop :: Dd tag -> Int
      zeep :: Char -> Dd tag
      zaaaaap :: Dd tag -> Dd tag
    

    Now you can write a Zoop instance for B (or 'B) and one for Z (or 'Z) to let users use the method for either. Remember, though, that types are erased in compilation, so you'll need a Zoop a constraint anytime you want to apply these methods with polymorphic tags.