[Haskell-cafe] specifying using type class
Ertugrul Söylemez
es at ertes.de
Mon Jul 23 16:08:03 CEST 2012
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>
More information about the Haskell-Cafe
mailing list