
Hi Todd,
Sorry, I will not answer your question, but discuss some points.
On Mon, Sep 26, 2016 at 7:48 AM, Todd Wilson
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]
What is the type of the union of an union ? For example : union fsmA (union fsmB fsmC) where fsmX are of type FSM x. Are you waiting for a triple (i.e. FSM (a, b, c)) or does a recursive tuple structures is ok ? (Such as FSM (a, (b, c))) such as your example depict ?
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)
As far as I understand depend type in Haskell, you cannot do that. You need to "pack" your "typed" FSM inside a existentially qualified generic fsm, such as : data AnyFSM = forall t. AnyFsm (FSM t) And then, later, "unpack" it using a case. However I think you also need a constraint on `t` else you will not be able to recover anything from it. Sorry, my knowledge stops here.
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]
As far as I know, and I'll be happy to be proven wrong here, you cannot write a function from a value to a type. However you can "promote" your value level RegExp to a type level 'RegExp (using the DataKind extension), and in this case, you will need to use tick in from of you promoted kind (such as 'Empty, or 'Plus), but as far as I know it is still impossible to write function this way, you need to write type families, something such as : type family f (t :: RegexExp) = * where f 'Empty = EmptyFSM f ('Letter a) = LetterFSM I apologies for this partial answer, but I'm interested by your question so I wanted to contribute at my level. -- Guillaume.