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