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

[Jason Dusek]

Is there a way to write a Haskell data structure that is
necessarily only one or two or seventeen items long; but
that is nonetheless statically guaranteed to be of finite
length?

--
Jason Dusek
Linux User #510144 | http://counter.li.org/
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Eugene Kirpichov]

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

2010/10/13 Jason Dusek <jason...@gmail.com>:

--
Eugene Kirpichov
Senior Software Engineer,
Grid Dynamics http://www.griddynamics.com/

[Max Bolingbroke]

On 13 October 2010 08:57, Jason Dusek <jason...@gmail.com> wrote:
>  Is there a way to write a Haskell data structure that is
>  necessarily only one or two or seventeen items long; but
>  that is nonetheless statically guaranteed to be of finite
>  length?

Maybe you want a list whose denotation is formed by a least (rather
than a greatest) fixed point? i.e. the type of spine-strict lists:

"""
data FinList a = Nil
| Cons a !(FinList a)
deriving (Show)

ones_fin = 1 `Cons` ones_fin

take_fin n Nil = Nil
take_fin n (Cons x rest)
| n <= 0 = Nil
| otherwise = Cons x (take_fin (n - 1) rest)

ones = 1 : ones

main = do
print $ take 5 ones
print $ take_fin 5 ones_fin
"""

If you have e :: FinList a then if e /= _|_ it is necessarily of finite length.

Max

[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

[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 <migue...@yandex.ru>:

--

Eugene Kirpichov
Senior Software Engineer,
Grid Dynamics http://www.griddynamics.com/

[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<migue...@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 О©╫О©╫О©╫О©╫О©╫:

[Eugene Kirpichov]

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
<migue...@yandex.ru> написал:

>  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<migue...@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
>>> Haskel...@haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>
>>
>

--

Eugene Kirpichov
Senior Software Engineer,
Grid Dynamics http://www.griddynamics.com/

[Steffen Schuldenzucker]

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
> <migue...@yandex.ru> О©╫О©╫О©╫О©╫О©╫О©╫О©╫:

>> 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<migue...@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 О©╫О©╫О©╫О©╫О©╫:

[Steffen Schuldenzucker]

Hmm, ok, I simplified the idea[1] and it looks like I'm getting the same
problem as you when trying to drop the 'n' parameter carrying the length of
the list.

Sad thing.

[1] http://hpaste.org/40538/finite_list__not_as_easy_as_i

[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
> <perm...@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
>>> <perm...@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 <migue...@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 О©╫О©╫О©╫О©╫О©╫:

[Jonas Almström Duregård]

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 <ekirp...@gmail.com>:

[Stephen Tetley]

Hi Jonas

Nice, but how about a list destructor?

;-)

[Jonas Almström Duregård]

> 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

[Ozgur Akgun]

Jonas,

2010/10/13 Jonas Almström Duregård <jonas.d...@chalmers.se>

(++) :: 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

[Jonas Almström Duregård]

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

Typo. Plus is sufficient. 

What I would really like is a nice way of implementing concat (i.e. concatenate a finite number of finite lists, of various "sizes", into a single finite list).

/J

2010/10/13 Ozgur Akgun <ozgur...@gmail.com>

[Brent Yorgey]

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

[Stephen Tetley]

Hi Jonas

Thanks - I was meaning an equivalent to viewl on Data.Sequence, on plain 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

[Jonas Almström Duregård]

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 <stephen...@gmail.com>:

[Jonas Almström Duregård]

>Then viewl can be defined anywhere,
>
>viewl :: Finite s a -> Either () (a, Finite s a)
>viewl = finite (Left ()) (Right . (,))

... or more like:

viewl :: Finite s a -> Either () (a, Finite s a)

viewl = finite (Left ()) (\a b -> Right (a,b))

/J

2010/10/13 Jonas Almström Duregård <jonas.d...@chalmers.se>

Hi Stephen,

[Stephen Tetley]

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.

[Jason Dusek]

Thanks everyone for your thoughtful replies. I might have
expected a referral to a paper; it's a pleasant surprise
to have these worked examples.

--
Jason Dusek
Linux User #510144 | http://counter.li.org/

[Daniel Peebles]

One option could be something like:

data Z

data S n

data Vec n a where

  Nil :: Vec Z a

  Cons :: a -> Vec n a -> Vec (S n) a

data Length n where

  One :: Length (S Z)

  Two :: Length (S (S Z))

  Seventeen :: Length (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))

data FixedVec a where

  FixedVec :: Legnth n -> Vec n a -> FixedVec a

But it's obviously rather cumbersome :)

[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.

/J

[Jason Dusek]

2010/10/13 Jonas Almström Duregård <jonas.d...@chalmers.se>:

> ...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".