formal language L

Logic/Language.hs

@@ -1,13 +1,30 @@
 module Logic.Language where
 
+type List a = [a]
+
 -- Formal language (/grammar/production system/whatever)
 class (Eq symbol, Show symbol) => Language symbol where
-  -- If Haskell had dependent types this could be generalized.
-  -- For now the languages I want to make use at most up to infer3.
-  infer0 :: [[symbol]]
-  infer1 :: [[symbol] -> [[symbol]]]
-  infer2 :: [[symbol] -> [symbol] -> [[symbol]]]
-  infer3 :: [[symbol] -> [symbol] -> [symbol] -> [[symbol]]]
+  isWellFormed :: [symbol] -> Bool
+
+  -- If Haskell had dependent types these could be generalized.
+
+  -- axiomN : N wffs -> theorem
+  axiom0 :: [[symbol]]
+  axiom1 :: [[symbol] -> [symbol]]
+  axiom2 :: [[symbol] -> [symbol] -> [symbol]]
+  axiom3 :: [[symbol] -> [symbol] -> [symbol] -> [symbol]]
+
+  -- inferN : N theorems -> theorem
+  -- (axiom0 and infer0 would mean the same thing.)
+  infer1 :: [[symbol] -> List [symbol]]
+  infer2 :: [[symbol] -> [symbol] -> List [symbol]]
+
+  axiom0 = []
+  axiom1 = []
+  axiom2 = []
+  axiom3 = []
+  infer1 = []
+  infer2 = []
 
 -- Convenience newtype so strings are less ugly
 newtype Seq symbol = Seq [symbol]