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

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:

...

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

I don't know too much about GADTs, but it works fine with fundeps: http://hpaste.org/40535/finite_list_with_fundeps (This is rather a draft. If anyone can help me out with the TODOs, I'd be happy.) -- Steffen On 10/13/2010 10:40 AM, Eugene Kirpichov wrote:

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

...

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:

...

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

So all you need is a program that checks if your functions terminate. How hard can it be, right? ;) Seriously though, since you would need static termination guarantees on all functions that produce lists, you will be severely restricted when working with them. It's like Haskell without general recursion... Anyway, here's a quick version where you can do cons, map and ++. The idea is that any function that results in a larger list also results in a larger type. Any function that works on finite lists of type a can have type "Finite s a" as a parameter and since the finite module only exports the limited : and ++ functions it should be safe. The inferred type of "safeLength = length . infinite" is "safeLength :: Finite s a -> Int" for instance. {-# Language EmptyDataDecls #-} module Finite ( emp , (-:) , map , (++) , infinite , module Prelude ) where import Prelude hiding ((++), map) import qualified Prelude data Z data S a data Plus a b newtype Finite s a = Finite {infinite :: [a]} deriving Show instance Functor (Finite n) where fmap f = Finite . fmap f . infinite emp :: Finite Z a emp = Finite [] (-:) :: a -> Finite n a -> Finite (S n) a (-:) a l = Finite $ a : (infinite l) infixr 5 -: (++) :: Finite s1 a -> Finite s2 a -> Finite (S (Plus s1 s2)) a (++) (Finite a) (Finite b) = Finite $ a Prelude.++ b infixr 5 ++ map = fmap /J 2010/10/13 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 :

...

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

-- Eugene Kirpichov Senior Software Engineer, Grid Dynamics http://www.griddynamics.com/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Nice, but how about a list destructor

I'm not sure what you mean by destructor, if you mean an eliminator for case analysis then you can make a function finite :: b -> (a -> Finite s1 a -> b) -> Finite s2 a -> b finite b _ (Finite []) = b finite _ f (Finite (x:xs)) = f x xs If you men functions that possibly remove elements from lists, then you can add definitions like these to the module: filter = onList . Prelude.filter tail = onList Prelude.tail onList :: ([a] -> [b]) -> Finite s a -> Finite s b onList f = Finite . f . infinite Don't export onList though! filter and map should be enough to define any list function you want outside the module. Note that the size-type doesn't correspond exactly to the size of the list, but that's not really a problem as long as you only want to guarantee finiteness. /J On 13 October 2010 16:41, Stephen Tetley wrote:

Hi Jonas

Nice, but how about a list destructor?

;-) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Hi Jonas

Thanks - I was meaning an equivalent to viewl on Data.Sequence, on plain

Hi Stephen, I'm not sure I see the problem. You can do what you require with the function i supplied (minus the typo). This is in the module (where the Finite constructor is exposed) finite :: b -> (a -> Finite s a -> b) -> Finite s a -> b finite b _ (Finite []) = b finite _ f (Finite (x:xs)) = f x (Finite xs) Then viewl can be defined anywhere, viewl :: Finite s a -> Either () (a, Finite s a) viewl = finite (Left ()) (Right . (,)) Why would you ever decrease the Peano numbers? It's just an upper bound, not an exact size. /J 2010/10/13 Stephen Tetley : lists:

viewl :: [a] -> Either () (a,[a]) viewl [] = Left () viewl (x:xs) = Right (x,xs)

It was a trick question because I can't see how you can do it without decrement on the Peano numbers.

Best wishes

Stephen

Hi Jonas Thanks - I was anticipating a type like this for the destructor: viewl :: Finite s a -> Either () (a, Finite (Predecessor s) a) I didn't appreciate that the size type in your code represented the upper bound and not the actual size. Best wishes Stephen

Jonas, 2010/10/13 Jonas Almström Duregård

(++) :: Finite s1 a -> Finite s2 a -> Finite (S (Plus s1 s2)) a (++) (Finite a) (Finite b) = Finite $ a Prelude.++ b infixr 5 ++

Why do you have the S in the return type of Finite.++ ? Ozgur

On Wed, Oct 13, 2010 at 12:13:29PM +0400, Eugene Kirpichov wrote:

Hm. This is not actually an answer to your question, just a "discussion starter", but still.

The code below typechecks, though actually it shouldn't: there's no type "n" such that "ones" is formed by the FL from some value of type List Int n. Or should it?

{-# 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

Fascinating. Doing ones' = Cons 1 ones' of course does not typecheck (as expected) with an occurs check error (can't unify n = S n). But ones = cons 1 ones does typecheck. And it makes sense: I can see why cons has the type it does, and given that type for cons this definition of ones is perfectly well-typed. But the upshot, which I had never considered, seems to be that existentially quantified types are allowed to be _|_. -Brent

2010/10/13 Jonas Almström Duregård :

...and you can always do

hack :: Vec n a -> FixedVec a hack x :: FixedVec undefined

Also I'm guessing 1, 2 and 17 are just examples, he really wants arbitrary length finite lists.

Indeed. Where I said "is necessarily" I meant "is not necessarily". -- Jason Dusek Linux User #510144 | http://counter.li.org/