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

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