Well, it's easy to make it so that lists are either finite or bottom,
but it's not so easy to make infinite lists fail to typecheck...
That's what I'm wondering about.
2010/10/13 Miguel Mitrofanov <miguelim...@yandex.ru>:
> hdList :: List a n -> Maybe a
> hdList Nil = Nothing
> hdList (Cons a _) = Just a
>
> hd :: FiniteList a -> Maybe a
> hd (FL as) = hdList as
>
> *Finite> hd ones
>
> this hangs, so, my guess is that ones = _|_
>
>
> 13.10.2010 12:13, Eugene Kirpichov пишет:
>>
>> {-# LANGUAGE ExistentialQuantification, GADTs, EmptyDataDecls #-}
>> module Finite where
>>
>> data Zero
>> data Succ a
>>
>> class Finite a where
>>
>> instance Finite Zero
>> instance (Finite a) => Finite (Succ a)
>>
>> data List a n where
>> Nil :: List a Zero
>> Cons :: (Finite n) => a -> List a n -> List a (Succ n)
>>
>> data FiniteList a where
>> FL :: (Finite n) => List a n -> FiniteList a
>>
>> nil :: FiniteList a
>> nil = FL Nil
>>
>> cons :: a -> FiniteList a -> FiniteList a
>> cons a (FL x) = FL (Cons a x)
>>
>> list123 = cons 1 (cons 2 (cons 3 nil))
>>
>> ones = cons 1 ones -- typechecks ok
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
--
Eugene Kirpichov
Senior Software Engineer,
Grid Dynamics http://www.griddynamics.com/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
