regex-type
Regular expression matching of Haskell types using nondeterministic finite automata
This is a playground for writing type-level code using TypeFamilies.
Available on hackage
Some examples that work:
-- encode the following regex: (Int | Char | (Bool -> Bool)) (String | (Int -> Bool))
regex :: ('[a, b] ~= ((Int :| Char :| (Bool -> Bool)) :> (String :| (Int -> Bool)))) => a -> b
regex = undefined
-- The type of these functions all match the regular expression defined in the type of regex
-- so they all typecheck
test1 :: Int -> String
test1 = regex
test2 :: Int -> Int -> Bool
test2 = regex
test3 :: Char -> String
test3 = regex
test4 :: Char -> Int -> Bool
test4 = regex
test5 :: (Bool -> Bool) -> Int -> Bool
test5 = regex
test6 :: (Bool -> Bool) -> String
test6 = regex
-- This doesn't satisfy the regex, and thus a type error occurs
test_wrong :: Int -> Bool
test_wrong = regex
-- Doesn't typecheck because the list doesn't satisfy the (Int*) regex.
test_wrong2 :: ('[Int, Int, Int, Int, Char] ~= (Rep Int)) => a -> a
test_wrong2 = id
-- test7 can only be called with a ~ Int
test7 :: ('[Int, Int, Int, Int, a] ~= (Rep Int)) => a -> a
test7 = idTODO:
- Improve performance
- Try converting the NFA to a DFA. I don't know if this will make it faster overall, as I suspect the automaton is reconstructed every time, which means an exponential complexity on each check with the DFA. Maybe an on-demand construction?
- Figure out if it's actually useful for anything