Type-level regular expressions

Latest on Hackage:

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow to host generated Haddocks.

BSD3 licensed by Csongor Kiss


Regular expression matching of Haskell types using nondeterministic finite automata

This is a playground for writing type-level code using TypeFamilies.

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 = id


  • Improve performance
  • Make it a proper library
  • 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
Depends on:
comments powered byDisqus