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

Hi Todd, I’m afraid dependent types in today’s Haskell are not for the faint-of-heart, or any but the most advanced students. Indeed, as I’ve been thinking about my new course on typed functional programming for the spring, I’ve debated on whether I should skip Haskell and go straight to Idris/Agda because of this. I won’t do that, I’ve decided, but this means I have to give up on some of the dependent-type material I’d like to cover. To be fair, *some* slices of dependently typed programming are accessible. Stephanie Weirich’s red-black tree GADT has much of the flavor of dependently typed programming without as much of the Haskell-induced awkwardness. There is a decent description of this example in https://themonadreader.files.wordpress.com/2013/08/issue221.pdf I hope this helps! Richard -=-=-=-=-=-=-=-=-=-=- Richard A. Eisenberg Asst. Prof. of Computer Science Bryn Mawr College Bryn Mawr, PA, USA cs.brynmawr.edu/~rae

On Sep 28, 2016, at 2:49 AM, Todd Wilson wrote:

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