jfdm / idris-containers Goto Github PK

There is a bit rotted quick check implementation for Idris out there. I do not have time nor knowledge to fix it. In the mean time there is a reasonable setup for testing. This needs expanding and de-duplication of test data and operations where appropriate.

• Graph Tests
• Set tests
• Tree Tests
• Dict tests
• Other tests.

I'm trying to build a basic Idris program that uses this library, and there is a problem:

$ idris --build test.ipkg
Entering directory `.\src'
idris.exe: Erasure/getArity: definition not found for Data.Tree.Empty
CallStack (from HasCallStack):
  error, called at src\Idris\Erasure.hs:605:20 in idris-1.3.2-J5ej6IrsDvx8J6Vzd0MiVR:Idris.Erasure

This is the Main.idr I'm trying to compile, but I don't think that matters:

module Main

import Data.AVL.Set

remove : Ord a => a -> Set a -> Set a
remove x = let to_remove = insert x empty
               in flip difference to_remove

example : Set Int
example = fromList [1, 2, 3]

main : IO ()
main = do
  putStrLn $ show $ Set.toList $ remove 3 example

The library itself builds and installs fine. Typechecking by itself (from Atom at least) also works.

Hi

I don't understand why equality, as currently defined for sets, would work at all. It seems to only act on the head.

If my point is correct, then how would you go at defining it? In particular, I'm trying to prove that the union of two sets built from lists using fromList is the same as another set built using fromList, by means of list permutations, but without much success.

After some improved tests it turns out that the dependently typed AVL tree is broken, and needs fixing.

Would you be up for a Traversable Instance for Dict over the values in the dictionary?
I defined it locally as:

Ord a => Functor (Dict a) where 
  map func x = fromList $ (\(a, b) => (a, func b)) <$> toList x
Ord a => Foldable (Dict a) where   
  foldr func = foldr $ const func
Ord a => Traversable (Dict a) where 
  traverse f x = fromList <$> (traverse (\(a, b) => (MkPair a) <$> f b) $ Data.AVL.Dict.toList x)

Several functions impose an Ord constraint that serves no apparent purpose. It looks like the root of the problem is the height function, but others that use height, or that use functions that use height, are also infected.

Idris is telling me several functions are not total with Idris 1.0. Specifically Data.AVL.Tree.rotLeft and Data.AVL.Tree.rotRight. I tried poking around to see if I could fix it, but I'm not well verse enough in Idris and it's been too long since I've thought about AVL trees.

I see no indication that it preserves the ordering invariant. What you probably actually want is a deletion function that also returns an indication of whether the deleted element was previously in the tree.

The current queue implementation does not work properly in a persistent setting. It also doesn't have much in the way of proof behind it. I've opened pull request #10 to add Okasaki-style Banker's queues. They're rather more complicated, so it's quite possible that we should keep the simpler ones as well for the times when they're appropriate.

There is a simple non-dependently typed implementation of RedBlack trees in the repository.

• The core tree implementation needs extending to provide non-additive manipulation functions: delete, merge, update.
• This implementation should be turned into a Key-Value pair structure.
• RedBlack versions of: Graph, Dict, Set, Tree, structures should be constructed.
• Dependently Typed version of RedBlack trees would be nice.

Unlike :: for List, insert on Dict seems to lose information so that I can't prove much about the results.

I wrote an analog of lookup that uses HasKey proofs (see below) and now I want to prove...

insertValue: DecEq k => Ord k => (key: k) -> (dict: Dict k v)
  -> keyValue key (insert key val dict) found = val

but I don't see how.

keyValue: (key: k) -> (dict: (Dict k v)) -> (pf: HasKey key dict)
  -> v
keyValue key (MkDict $ Element t inv) (IsKey (IsKey found)) =
  keyValue' key t found
    where
      keyValue': (key: k) -> (t: Tree k v) -> (found: IsKeyIn key t) -> v
      keyValue' key (Node key val _ _) Here = val
      keyValue' key (Node not_key val left r) (InRight later) =
        keyValue' key r later
      keyValue' key (Node not_key val l right) (InLeft later) =
        keyValue' key l later

There are two types of AVL tree implementation in this project. The first, is a 'standard' implementation of AVL trees that was taken and adapted from Haskell. The second, uses dependent types to ensure that only balanced trees can be constructed.

There are issues with these implementations:

1. The standard AVL tree implementation has rotation issues. The entire balancing portion needs updating.
2. The Dependently Typed AVL came with a flaw in the left rotation functions. These need numpty checking. The affected lines are marked.
3. The Dependently Typed AVL is too strict in keeping the balance invariant true; the shape of the data structure remains fixed unless something is inserted. This will result in inefficient operations for manipulating structures---there are no in-place modifications. If the balancing invariant could be weakened to allow 'out of balance' trees, then removal and splitting and thus efficient manipulation functions could be constructed---merge,split,remove,update.

Update
This issue was partially addressed by provision of a dependently typed AVL tree implementation with the invariants separated. However, there is a yet to be diagnosed problem with rotation, it is lossy.