[Haskell-cafe] A question on dependent types in Haskell
Richard Eisenberg
rae at cs.brynmawr.edu
Wed Sep 28 16:39:06 UTC 2016
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.
>>
>>
More information about the Haskell-Cafe
mailing list