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

[Todd Wilson]

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 <li-yao.xia at ens.fr> wrote:
> 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.
>>
>