[Haskell-cafe] A question on dependent types in Haskell

[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.
>