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

26 Sep 2016

      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