Deriving data structures for logic programming

The problem

Consider the type of lists in Haskell:

data [a] = [] | a : (List a)

The naïve approach to adopting this type for logic programming is to instantiate it with the type of logic variables, which in turn are polymorphic:

data LogicVal a = Var Id | Val a
type BadLogicList a = [(LogicVal a)]

Although suitable for simple logic programs, this type is not suitable in general. While the head of a non-empty BadLogicList may be either fresh or ground, the tail must always be ground (up to WHNF). Therefore, every BadLogicList must either be finite or contain ⟂. This precludes writing many interesting logic programs.

Manual approach

We can create a suitable list structure by introducing a new datatype, rather than instantiating the original [a]:

data LogicList a = Nil | Cons (LogicVal a) (LogicVal (LogicList a))

This structure accounts for the possibility that both the head and the tail may be fresh, and so we may represent potentially-infinite lists (e.g., Cons (Var 0) (Var 1) corresponds to (_.0 . _.1)).

To go between [a] and LogicList a without much pain, we can define the partial bijection fromList/toList (partial because we may encounter non-ground values):

fromList :: [a] -> LogicList a
fromList []     = Nil
fromList (x:xs) = Cons (Val x) (Val $ fromList xs)

toList :: LogicList a -> Maybe [a]
toList Nil                     = return []
toList (Cons (Val x) (Val xs)) = (:) x <$> toList xs
toList _                       = mzero

Boilerplate explosion

There are many difficulties with this solution, though. Since we introduce a new type, we can no longer directly use existing functions for the old type. This seems appropriate, though, since the semantics of existing functions are unclear in the presence of potentially non-ground values. The amount of boilerplate required to introduce this new type is a bigger problem. Consider the ordinary representation of the term language from Infer.hs:

data Exp = VarE    Id
         | IntE    Int
         | BoolE   Bool
         | IsZeroE Exp
         | PredE   Exp
         | MultE   Exp  Exp
         | IfE     Exp  Exp Exp
         | LamE    Id   Exp
         | AppE    Exp  Exp
           deriving (Eq, Show)

To make this logic-programming friendly, we must introduce quite a few extra type constructors:

data Exp = VarE    (LogicVal Id)
         | IntE    (LogicVal Int)
         | BoolE   (LogicVal Bool)
         | IsZeroE (LogicVal Exp)
         | PredE   (LogicVal Exp)
         | MultE   (LogicVal Exp)  (LogicVal Exp)
         | IfE     (LogicVal Exp)  (LogicVal Exp) (LogicVal Exp)
         | LamE    (LogicVal Id)   (LogicVal Exp)
         | AppE    (LogicVal Exp)  (LogicVal Exp)
           deriving (Eq, Show)

Any functions which operate on this type must contain a substantial amount of boilerplate as well. Since such functions must be written to instantiate the Unifiable and Reifiable instances, this is quite a burden to meet before you can use the type in a logic program.

Generic approaches

Haskell data types can be represented as a sum of products along with a unit. For example, Maybe a ≅ 1 + a, [a] ≅ 𝜇X. 1 + a * X. To use an arbitrary type in a logic programming setting, it is sufficient to apply the metafunction logicize to the types as follows:

• logicize(1) = Id + 1
• logicize(t + t) = Id + (logicize(t) + logicize(t))
• logicize(t * t) = Id + (logicize(t) * logicize(t))

Derive new data type

One way to implement logicize would be via Template Haskell. This would probably require access to the source of the original type's declaration, and possibly would introduce a bunch of naming ugliness (e.g., prefixed names for derived types and constructors).

Use GHC generic programming facilities

Several options exist for generic programming in GHC:

• Preliminary support in GHC itself: http://www.haskell.org/ghc/docs/latest/html/users_guide/generic-programming.html
• Library that's similar at first glance to GHC's built-in generics: http://hackage.haskell.org/package/instant-generics

These tools might be used to implement something that looks very much like the logicize metafunction. It might be possible to avoid the creation of a new data type by making default instances of Unifiable that keep the raw U/:+:/:*: representations in the substitution. This could of course be overridden for types where unification should have a semantic meaning that doesn't correspond to a tree-unify of its concrete structures (e.g., a hash table).

The difficulty here would be in allowing the user to fill in holes in the lifted structures, backquote and comma style. It might be possible to use some Template Haskell here, but I'm not sure.