Hi I'm trying to write a proof checker in Haskell. One way of representing terms is as follows:

data Term = Const String | Fun String [Term] | Var String

But this seems unideal, since String can take on many values and there is no way of verifying the arity of function terms.

One solution is as follows:

data Term a = Const String | Fun a | Var String
data NTFun = S (Term NTFun) | Plus (Term NTFun) (Term NTFun)
type NTTerm = Term NTFun

Now I have a more generic Term type and can instantiate it as I please. But if I want to abstract out constant symbols as well it gets messy.

data Term a c = Const c | Fun a | Var String
data NTFun c = S (Term c (NTFun c)) | Plus (Term c (NTFun c)) (Term c (NTFun c))
data NTConst = Zero
type NTTerm = Term (NTFun NTConst) NTConst

It seems there must be a better way to express this? Thanks!

CodePudding user response：

You can change NTFun to be a functor, abstracting out its mentions of Term and any of its other variables, and have Term itself tie the knot.

data Term f c = Const c | Fun (f (Term f c)) | Var String
data NTFun term = S term | Plus term term
data NTConst = Zero
type NTTerm = Term NTFun NTConst