Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Get rid of extra indirections (WIP) #25

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

treeowl
Copy link
Contributor

@treeowl treeowl commented Oct 21, 2020

Setting out to implement the ideas in #12.

  • Store a Vector_ in the root node instead of an
    Array of Vector_s. This simplifies almost everything
    and should make the code smaller. This seems especially
    important for folds, which we generally want to inline. But
    we get one extra indirection per vector until we actually
    unlift everything.

  • Make Vector_ a GADT. This lets us use the type system to
    enforce the height balance invariant. Ultimately, this is going
    to have to look different, but I think it's not a bad first step.

  • Add a validity test to check the rest of the data structure
    invariants.

@treeowl treeowl marked this pull request as draft October 21, 2020 20:46
* Store a `Vector_` in the root node instead of an
  `Array` of `Vector_`s. This simplifies almost everything
  and should make the code smaller. This seems especially
  important for folds, which we generally want to inline.

* Make `Vector_` a GADT. This lets us use the type system to
  enforce the height balance invariant.

* Add a validity test to check the rest of the data structure
  invariants.
@treeowl
Copy link
Contributor Author

treeowl commented Oct 30, 2020

A couple thoughts:

  1. I think I actually want to work mostly with UnliftedArray# rather than UnliftedArray. So I probably want a module providing relatively user-friendly operations on UnliftedArray# (using Int rather than Int#, using ST with Box rather than explicit state-token passing, etc).

  2. To make things as backwards compatible as possible, use a data family rather than an injective type family. But we want to discard those newtype constructors with as little fuss as possible. I'm developing a pretty decent sense of how I think I want that to work.

@treeowl
Copy link
Contributor Author

treeowl commented Oct 30, 2020

There is another alternative to working mostly with UnliftedArray#, I think. The idea is to generalize Array and UnliftedArray to a unified type. This will be annoying, but it might shift the burden of ugliness into a simpler space.

-- Keep the kind open to support unboxed arrays?
data L
data U
type family Blob (l :: Type) (a :: Type) :: TYPE 'UnliftedRep
type instance Blob L a = Array# a
type instance Blob U a = UnliftedArray# (Unlifted a)

data Array (l :: Type) (a :: Type) = Array (Blob l a)

What's this do? It lets us yank an Array out of an Array 'U without having to determine whether it's actually an Array# or an UnliftedArray#.

@treeowl
Copy link
Contributor Author

treeowl commented Oct 30, 2020

No, that second thing isn't quite right. We need to add in an assumption that an Array U holds an Array x... hmm... Might not work out.

@treeowl
Copy link
Contributor Author

treeowl commented Oct 30, 2020

Yeah, I think I'm going with the first idea. It sucks, but at least I know how to make it work.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant