[Haskell-cafe] Finite but not fixed length...
Permjacov Evgeniy
permeakra at gmail.com
Wed Oct 13 07:31:38 EDT 2010
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
>>>>>>
>>>
>>
>
>
More information about the Haskell-Cafe
mailing list