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

[Richard Eisenberg]

Hi Todd,

My `singletons` library kludges dependent types into Haskell via much dirty Template Haskell hackery. But it works in your use case. I was able to write your reg2fsm function much as you desired.

See attached.

Note that my type signature for reg2fsm (`Sing (r :: RegExp) -> FSM (F r)`) is essentially a dependent type: you can view `Sing (r :: RegExp)` to be like an argument `(r : RegExp)` in a proper dependently-typed language. Alternatively, you can pronounce `Sing` as `Π`.

Richard

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Regex.hs
Type: application/octet-stream
Size: 1842 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160927/1ff3a30e/attachment.obj>
-------------- next part --------------

-=-=-=-=-=-=-=-=-=-=-
Richard A. Eisenberg
Asst. Prof. of Computer Science
Bryn Mawr College
Bryn Mawr, PA, USA
cs.brynmawr.edu/~rae

> On Sep 26, 2016, at 1:48 AM, Todd Wilson <twilson at csufresno.edu> 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.