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

[Permjacov Evgeniy]

 infinite value is value, that have no upper bound (see infinity
definition). So, you have to provide upper bound at compile time. Tree
example provides such bound.

On 10/13/2010 03:27 PM, Eugene Kirpichov wrote:
> Again, the question is not how to arrange that all non-bottom values
> are finite: this can easily be done using strictness, as in your List
> example.
>
> The trick is to reject infinite values in compile time. How can *this* be done?
>
> 13 октября 2010 г. 15:26 пользователь Permjacov Evgeniy
> <permeakra at gmail.com> написал:
>>  On 10/13/2010 03:09 PM, Eugene Kirpichov wrote:
>>
>> 1-st scenario: If you have, for example, 2-3 tree, it definitly has a
>> root. If you construct tree from list and then match over root, the
>> entire tree (and entire source list) will be forced. And on every
>> update, 2-3 tree's root is reconstructed in functional setting. So, if
>> you'll try to build 2-3 tree from infinite list, it will fail in process
>> due insuffisient memory.
>> Of course, you can make the same with
>>  data List a = Cons a (!List a) | Nil
>>
>> second scenario
>> data Node a = Nil | One a | Two a a
>> and so Node (Node (Node (Node a))) has at most 2^4 = 16 elements. with
>> some triks you'll be able to set upper bound in runtime.
>>
>>> I don't see how. Could you elaborate?
>>>
>>> 13 октября 2010 г. 14:46 пользователь Permjacov Evgeniy
>>> <permeakra at gmail.com> написал:
>>>>  On 10/13/2010 12:33 PM, Eugene Kirpichov wrote:
>>>> I think, tree-like structure, used as sequence (like fingertrees), will
>>>> do the work.
>>>>> 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
>>>>>>
>>>
>>
>
>