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

[Richard Eisenberg]

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 <twilson at csufresno.edu> 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 <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.
>> 
>>