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

13 Oct 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
 написал:
...
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
 написал:
...
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 :
...
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