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

[Guillaume Bouchard]

Hi Todd,

Sorry, I will not answer your question, but discuss some points.

On Mon, Sep 26, 2016 at 7:48 AM, Todd Wilson <twilson at csufresno.edu> wrote:

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