[Haskell-cafe] specifying using type class

[Ertugrul Söylemez]

Patrick Browne <patrick.browne at dit.ie> wrote:

> Thank you for your clear an detailed reply, the work on dependent
> types seems to address my needs. However it is beyond my current
> research question, which is quite narrow(see[1]). I merely wish to
> identify the strengths and weakness of *current Haskell type classes*
> as a pure *unit of specification*. I do not wish to address any
> perceived weakness, I merely wish to identify them (if there are
> ant). Of course my question may be ill conceived, in that type classes
> were intended to specify interfaces and not algebraic types.

Oh, now I get what you really want.  You want to specify not only the
captured operations, but also assumptions about them.  This is not
impossible in Haskell, but in most cases you will need at least some
form of lightweight dependent types.  However, this can only prove
certain properties, which are not dependent on the functions themselves,
but only their types.  Here is a variant of Stacklike that does static
length checks (GHC 7.4 required):

    {-# LANGUAGE DataKinds, GADTs, KindSignatures, RankNTypes #-}

    data Nat = Z | S Nat

    data Stack :: Nat -> * -> * where
        Empty :: Stack Z a
        Push  :: a -> Stack n a -> Stack (S n) a

    class Stacklike (s :: Nat -> * -> *) where
        emptyStack :: s Z a
        pop        :: s (S n) a -> (a, s n a)
        push       :: a -> s n a -> s (S n) a
        size       :: s n a -> Nat
        toList     :: s n a -> [a]

        fromList :: [a] -> (forall n. s n a -> b) -> b
        fromList [] k = k emptyStack
        fromList (x:xs) k = fromList xs (k . push x)

    instance Stacklike Stack where
        emptyStack      = Empty
        pop (Push x xs) = (x, xs)
        push            = Push

        size Empty = Z
        size (Push _ xs) = S (size xs)

        toList Empty = []
        toList (Push x xs) = x : toList xs

Here it is statically proven by Stacklike that the following length
preserving property holds:

    snd . pop . push x :: (Stacklike s) => s n a -> s n a

The way Stack is defined makes sure that the following holds:

    (snd . pop . push x) emptyStack = emptyStack

These are the things you can prove.  What you can't prove is properties
that require lifting the class's functions to the type level.  This
requires real dependent types.  You can replicate the functions on the
type level, but this is not lifting and can introduce errors.

Also for real proofs your language must be total.  Haskell isn't, so you
can always cheat by providing bottom as a proof.  You may want to check
out Agda.


Greets,
Ertugrul

-- 
Not to be or to be and (not to be or to be and (not to be or to be and
(not to be or to be and ... that is the list monad.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120723/80d67ca7/attachment.pgp>