I actually tried the approach of indexing the RegExp type before, but
I didn't like it for the reason you indicated: I was also using RegExp
for many other purposes that have nothing to do with FSMs and I didn't
want to be forced to include the superfluous type indices in those
situations. On the other hand, for the reg2fsm function, I wanted to
use the extra type information to limit the space of solutions: the
existence of my function f :: RegExp -> * was meant to guide the
constructions that students might write.
--Todd
On Mon, Sep 26, 2016 at 1:51 AM, Li-yao Xia
Hello Todd,
This seems like a neat place to use GADTs!
Instead of trying to define f :: RegExp -> * by fully lifting RegExp to the type level, you can use GADTs to reflect the structure of a RegExp in its type:
data RegExp a where -- a is the state type of the FSM associated with the regexp Empty :: RegExp EmptyFSM Letter :: RegExp LetterFSM Plus :: RegExp a -> RegExp b -> RegExp (a, b) Cat :: RegExp a -> RegExp b -> RegExp (a, [b]) Star :: RegExp a -> RegExp [a]
reg2fsm :: Eq a => RegExp a -> FSM a -- ^ I assume you'll need an Eq constraint here to normalize -- the "non-deterministic states".
It may be much less flexible than what you originally intended, because the RegExp type is now tied to your FSM implementation. RegExps might also become painful to pass around because of their too explicit type. If that happens to be the case, you can clean up an API which uses this regexp with an existential wrapper.
data SomeRegExp where SomeRegExp :: Eq a => RegExp a -> SomeRegExp
data SomeFSM where SomeFSM :: Eq a => FSM a -> SomeFSM
Another simpler solution is to only use such a wrapper around FSM (i.e., your output), keeping the RegExp type as you first wrote it. You'd have:
reg2fsm :: RegExp -> SomeFSM
Here you totally lose the relationship between the RegExp and the FSM, so it seems to move away from what you were looking for. But if ultimately you don't care about the actual type of the state of a FSM, this gets the job done.
Regards, Li-yao
On 09/26/2016 06:48 AM, Todd Wilson wrote:
I haven't yet had the pleasure of exploring the subtleties of dependently-typed programming in Haskell, but I'm finding myself in need of a little bit of it in advance of that exploration and was hoping for some suggestions.
I have a type of regular expressions:
data RegExp = Empty | Letter Char | Plus RegExp RegExp | Cat RegExp RegExp | Star RegExp
and a type of (deterministic) finite state machines that is polymorphic in the state type:
data FSM a = FSM { states :: [a], start :: a, finals :: [a], delta :: [(a,Char,a)] }
I've fixed an alphabet sigma :: [Char], and I want to write the function that converts a regular expression to its associated FSM. The machines associated with Empty and Letter are given by
data EmptyFSM = Etrap emptyFSM :: FSM EmptyFSM emptyFSM = FSM { states = [Etrap], start = Etrap, finals = [], delta = [(Etrap, c, Etrap) | c <- sigma] }
data LetterFSM = Lstart | Lfinal | Ltrap letterFSM :: Char -> FSM LetterFSM letterFSM c = FSM { states = [Lstart, Lfinal, Ltrap], start = Lstart, finals = [Lfinal], delta = [(Lstart, c', if c' == c then Lfinal else Ltrap) | c' <- sigma] ++ [(q, c', Ltrap) | q <- [Lfinal, Ltrap], c' <- sigma] }
Suppose I can code the constructions of the union machine, concatenation machine, and star machine so that they have the types
unionFSM :: FSM a -> FSM b -> FSM (a,b) catFSM :: FSM a -> FSM b -> FSM (a,[b]) starFSM :: FSM a -> FSM [a]
Now what I want to do is to put all of this together into a function that takes a regular expression and returns the associated FSM. In effect, my function should have a dependent type like
reg2fsm :: {r : RegExp} -> FSM (f r)
where f is the function
f :: RegExp -> * f Empty = EmptyFSM f (Letter a) = LetterFSM f (Plus r1 r2) = (f r1, f r2) f (Cat r1 r2) = (f r1, [f r2]) f (Star r) = [f r]
and be given by
reg2fsm Empty = emptyFSM reg2fsm (Letter c) = letterFSM c reg2fsm (Plus r1 r2) = unionFSM (reg2fsm r1) (reg2fsm r2) reg2fsm (Cat r1 r2) = catFSM (reg2fsm r1) (reg2fsm r2) reg2fsm (Star r) = starFSM (reg2fsm r)
What is the suggested approach to achieving this in Haskell?
-- Todd Wilson A smile is not an individual Computer Science Department product; it is a co-product. California State University, Fresno -- Thich Nhat Hanh _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.