[Haskell-cafe] Finite but not fixed length...

[Eugene Kirpichov]

Well, in my implementation it's indeed impossible. It might be
possible in another one. That is the question :)
Perhaps we'll have to change the type of cons, or something.

13 октября 2010 г. 12:37 пользователь Miguel Mitrofanov
<miguelimo38 at yandex.ru> написал:
>  So... you want your "ones" not to typecheck? Guess that's impossible, since
> it's nothing but "fix" application...
>
> 13.10.2010 12:33, Eugene Kirpichov пишет:
>>
>> 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<miguelimo38 at 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 at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>
>>
>



-- 
Eugene Kirpichov
Senior Software Engineer,
Grid Dynamics http://www.griddynamics.com/