I am using Haskell to implement the text book algorithms on automata
theory and formal languages. In the moment I'd like to implement the
algorithm which translates regular expressions (RegExp) to nondeterministic
finite automata (NFA). I.e. I have defined the types (ignore Fin
(=finite type) for the moment):
data (Fin q,Fin sigma) =>
NFA q sigma = NFA {delta :: (q,sigma) -> [q], q0 :: [q], fin :: q -> Bool}
deriving Show
..
data RegExp sigma = Empty | Epsilon | Sym sigma
| Seq (RegExp sigma,RegExp sigma)
| Alt (RegExp sigma,RegExp sigma)
| Star (RegExp sigma)
Now since the type of states depends on the regular expression (and
Haskell has no dependent types so far) it seems reasonable to use an
existential type:
data (Fin sigma) => NFA' sigma = forall q. (Fin q) => NFA' (NFA q sigma)
and I'd like to define
re2nfa :: (Fin sigma) => (RegExp sigma) -> (NFA' sigma)
re2nfa Empty = NFA' a_empty
re2nfa Epsilon = NFA' a_epsilon
re2nfa (Sym x) = NFA' (a_sym x)
re2nfa (Seq (e1,e2)) = let NFA' a1 = re2nfa e1
NFA' a2 = re2nfa e2
in NFA' (a_seq a1 a2)
re2nfa (Alt (e1,e2)) = let NFA' a1 = re2nfa e1
NFA' a2 = re2nfa e2
in NFA' (a_alt a1 a2)
re2nfa (Star e) = let NFA' a = re2nfa e
in NFA' (a_star a)
where
a_empty :: Fin sigma => NFA () sigma
a_epsilon :: Fin sigma => NFA () sigma
a_sym :: Fin sigma => sigma -> NFA Bool sigma
a_seq :: (Fin sigma,Fin q1,Fin q2) =>
(NFA q1 sigma) -> (NFA q2 sigma) -> (NFA (Either q1 q2) sigma)
a_alt :: (Fin sigma,Fin q1,Fin q2) =>
(NFA q1 sigma) -> (NFA q2 sigma) -> (NFA (Either q1 q2) sigma)
a_star :: (Fin sigma,Fin q) => (NFA q sigma) -> (NFA (Maybe q) sigma)
the complete code is available from
http://www.tcs.informatik.uni-muenchen.de/~alti/drafts/automata.zip
However, I get error messages form hugs -98
ERROR "RegExp.hs" (line 54): Inferred type is not general enough
*** Expression : re2nfa
*** Expected type : Fin a => RegExp a -> NFA' a
*** Inferred type : Fin _37 => RegExp _37 -> NFA' _37
and from ghc -fglasgow-exts
RegExp.hs:57:
My brain just exploded.
I can't handle pattern bindings for existentially-quantified constructors.
In the binding group
NFA' a1 = re2nfa e1
In the right-hand side of an equation for `re2nfa':
let
NFA' a1 = re2nfa e1
NFA' a2 = re2nfa e2
in NFA' (a_seq a1 a2)
among others.
Did I encounter a limitation of the implementationbs of existential
types or is there just a stupid bug in my code?
If it is a limitation the next question is whether there is a
reasonable workaround apart from the obvoius one of defining the
disjoint union of all possible state types.
Thorsten
