40 lines
1.1 KiB
Haskell
40 lines
1.1 KiB
Haskell
module Logic.Language where
|
|
|
|
-- Convenience newtype so strings of symbols are less ugly
|
|
newtype ConcatShowList symbol = ConcatShowList [symbol]
|
|
instance Show a => Show (ConcatShowList a) where
|
|
show (ConcatShowList xs) = concat $ map show xs
|
|
|
|
-- Formal language (/grammar/production system/whatever)
|
|
-- https://en.wikipedia.org/wiki/Post_canonical_system
|
|
class Show symbol => Language symbol where
|
|
isWellFormed :: [symbol] -> Bool
|
|
|
|
-- If Haskell had dependent types these could be generalized.
|
|
|
|
-- axiomN : N wffs -> theorem
|
|
axiom0 :: [TypeAxiom0 symbol]
|
|
axiom1 :: [TypeAxiom1 symbol]
|
|
axiom2 :: [TypeAxiom2 symbol]
|
|
axiom3 :: [TypeAxiom3 symbol]
|
|
|
|
axiom0 = []
|
|
axiom1 = []
|
|
axiom2 = []
|
|
axiom3 = []
|
|
|
|
-- inferN : N theorems -> theorem
|
|
-- (axiom0 and infer0 would mean the same thing.)
|
|
infer1 :: [TypeInfer1 symbol]
|
|
infer2 :: [TypeInfer2 symbol]
|
|
|
|
infer1 = []
|
|
infer2 = []
|
|
|
|
type TypeAxiom0 s = [s]
|
|
type TypeAxiom1 s = [s] -> [s]
|
|
type TypeAxiom2 s = [s] -> [s] -> [s]
|
|
type TypeAxiom3 s = [s] -> [s] -> [s] -> [s]
|
|
|
|
type TypeInfer1 s = [s] -> [[s]]
|
|
type TypeInfer2 s = [s] -> [s] -> [[s]]
|