Haskell nested lists with newtype-CodePudding

Disclaimer: I am new to working with haskell.

I am working with proving logical formulas in haskell. I have trouble understanding how to work with newtypes and datas properly.

I have defined the following types to represent logical formulas that have the structure: (a or b or c) and (d or e) and (f) etc.

data Literal x = Literal x | Negation x
  deriving (Show, Eq)

newtype Or x = Or [Literal x]
  deriving (Show, Eq)

newtype And x = And [Or x]
  deriving (Show, Eq)

I want to write a function that can filter on the literals (i.e. take out certain a b or c based on some condition). Naively I thought this should be similar to filtering on [[Literal x]] but I cannot seem to get it to work.

My current method is something like:

filterLit :: Eq x => And x -> And x
filterLit = map (\(Or x) -> (filter (\(Lit l) -> condition l) x))

This doesn't type. I feel like I'm missing some syntax rules here. Let me know if you have suggestions on how I should approach it.

CodePudding user response：

\(Or x) -> filter (\(Lit l) -> condition l) x

Let's check the type of this function.

The domain must have type Or x. That's OK.

The codomain is the result of filter, hence it is a list. Let's only write [....] for that.

Hence, the function is Or x -> [....].

If we map that, we get [Or x] -> [[....]]. This is not the same as the claimed type And x -> And x -- a type error is raised.

First, you want your lambda to have type Or x -> Or x. For that, you can use \(Or x) -> Or (filter .....).

Then, you want filterLit to be something like

filterLit (And ys) = And (map ....)

so that it has the right type.