[Haskell-cafe] A question on dependent types in Haskell
Richard Eisenberg
rae at cs.brynmawr.edu
Tue Sep 27 15:28:28 UTC 2016
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.
More information about the Haskell-Cafe
mailing list