[Haskell-cafe] Re: (more) type level functions (type of decreasing list)

[Greg Buchholz]

oleg at pobox.com wrote:
] 
] One way is to use existentials:
] 

> data Seq1 a = forall b. (Pre a b, Show b) => Cons1 a (Seq1 b) | Nil1

] 
] which perhaps not entirely satisfactory because we have to specify all
] the needed classes in the definition of Seq1.

    Yes, that seems pretty burdensome, since we can't now create even a
simple function like "tail", right?  Or at least I think existentials
are the problem with this...

> tail1 :: (Pre a b, Show b) => Seq1 a -> Seq1 b
> -- tail1 (Cons1 x xs) = xs
> tail1 Nil1 = error "empty Seq"

...ghci reports...

    Couldn't match expected type `b' (a rigid variable)
           against inferred type `b1' (a rigid variable)
      `b' is bound by the type signature for `tail_' at dec2.lhs:30:17
      `b1' is bound by the pattern for `Cons1' at dec2.lhs:31:8-17
      Expected type: Seq1 b
      Inferred type: Seq1 b1
    In the expression: xs
    In the definition of `tail1': tail1 (Cons1 x xs) = xs

...and hugs...

 ERROR "dec2.lhs":31 - Existentially quantified variable in inferred type
 *** Variable     : _3
 *** From pattern : Cons1 x xs
 *** Result type  : Seq1 _0 -> Seq1 _3

] 
] Perhaps a better -- and a more general alternative -- is to use
] type-level programming to its fullest. The following defines a list
] whose elements are constrained to be in the decreasing, increasing,
] or any other (defined in the future) order. This example shows that
] Haskell truly has more kinds than it is commonly acknowledged.

<snip>

] > data Cons a b = Cons a b
] > data Nil = Nil

...if we build our lists with tuple-like Conses, our types end up being
as long as our lists, right?  So an infinite list has an infinite type,
which seems like it could be problematic to type check.  For example,
here's an arbitrarly long increasing list...

> data Seq' a = Cons' a (Seq' (Succ a)) | Nil' deriving Show
>
> from :: a -> Seq' a
> from x = Cons' x (from (S x))
>
> inf = from Z

...with some of the usual functions...

> tail_ :: Seq' a -> Seq' (Succ a)
> tail_ (Cons' x xs) = xs
>
> class Take a where 
>     take_ :: a -> (Seq' b) -> (Seq' b)
>
> instance Take Zero where 
>     take_ Z _ = Nil'
> 
> instance Take a => Take (Succ a) where
>     take_ (S n) (Cons' x xs) = Cons' x (take_ n xs)
>     take_ _ Nil' = error "can't take_ that many"
>
> class Drop a b c | a b -> c where
>     drop_ :: a -> Seq' b -> Seq' c
>
> instance Drop Zero b b where
>     drop_ Z xs = xs
>
> instance Drop a (Succ b) c => Drop (Succ a) b c where
>     drop_ (S n) (Cons' x xs) = drop_ n xs
>     drop_ _ Nil' = error "can't drop_ that many"

...Anyway, for fun, here's a list that alternates between two types in a
linearly increasing manner.  So you can start out with one Int and then
two Strings, then three Ints, four Strings, etc.  I don't know if it is
going to yeild to a type classless GADT solution yet, but I'll keep
thinking about it.

>
> data Fancy a b left next =  
>     forall c d left' next' lz decleft .
>     (Show c, Show d,
>      Zerop left lz,
>      If lz (Succ next) next next',
>      Pre left decleft,
>      If lz next decleft left',
>      If lz b a c,
>      If lz a b d
>     ) => Cons a (Fancy c d left' next') | Nil
> 
> fancy :: Fancy Integer String Zero (Succ Zero)
> fancy = (Cons 1 
>         (Cons "a" (Cons "b" 
>         (Cons  2  (Cons  3  (Cons 4 
>         (Cons "c" (Cons "d" (Cons "e" (Cons "f"
>         (Cons  5  (Cons  6  (Cons  7  (Cons  8  (Cons 9 Nil)))))))))))))))
>
> instance (Show a, Show b) => Show (Fancy a b c d) where
>     show (Cons x xs) = "(Cons " ++ (show x) ++ " " ++ (show xs) ++ ")"
>     show Nil = "Nil"
>
> data Succ a = S a deriving Show
> data Zero = Z deriving Show 
> 
> data TTrue
> data TFalse
> 
> class Pre a b | a -> b 
> instance Pre (Succ a) a
> instance Pre Zero Zero
> 
> class If p t e result | p t e -> result
> instance If TTrue  a b a
> instance If TFalse a b b
> 
> class Zerop a b | a -> b
> instance Zerop Zero TTrue
> instance Zerop (Succ a) TFalse
>