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

[Todd Wilson]

Richard,

Thanks for this suggestion. I wasn't aware of the singletons library;
I'll have to take a look.

To you and the other readers of this thread: are there other
approaches that have not yet been suggested? Since I'm using this for
a series of assignments for students that have seen Haskell before but
are still relative beginners, I'm looking for something that will be
relatively easy to explain, won't get in the way of them writing the
constructions in the straightforward way, and yet will provide some
additional type-checking to help catch their errors.

--Todd

On Tue, Sep 27, 2016 at 8:28 AM, Richard Eisenberg <rae at cs.brynmawr.edu> wrote:
> 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 <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.
>
>