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

Specialization optimization assumes that all type variables are at the front #2945

Closed
lukaszcz opened this issue Aug 8, 2024 · 0 comments · Fixed by #2944
Closed

Specialization optimization assumes that all type variables are at the front #2945

lukaszcz opened this issue Aug 8, 2024 · 0 comments · Fixed by #2944
Assignees
Milestone

Comments

@lukaszcz
Copy link
Collaborator

lukaszcz commented Aug 8, 2024

The specialization optimization in Core assumes that all type variables come first.

This assumption is not true, e.g., for for and rfor here:

instance
foldableRangeI {N} {{Ord N}} {{Natural N}} : Foldable (Range N) N :=
  mkFoldable@{
    for {B : Type} (f : B -> N -> B) (ini : B) : Range N -> B
      | (mkRange low high step) :=
        let
          {-# specialize-by: [f] #-}
          terminating
          go (acc : B) (next : N) : B :=
            if
              | next > high := acc
              | else := go (f acc next) (next + step);
        in go ini low;
    rfor {B : Type} (g : B -> N -> B) (ini : B) : Range N -> B
      | (mkRange low high step) :=
        let
          {-# specialize-by: [g] #-}
          terminating
          go (base : B) (next : N) : B :=
            if
              | next <= high := g (go base (next + step)) next
              | else := base;
        in go ini low
  };
@lukaszcz lukaszcz added this to the 0.6.5 milestone Aug 8, 2024
@lukaszcz lukaszcz self-assigned this Aug 8, 2024
@lukaszcz lukaszcz added core Related to JuvixCore optimization labels Aug 8, 2024
@lukaszcz lukaszcz changed the title Various parts of the pipeline assume that all type variables are at the front Specialization optimization assumes that all type variables are at the front Aug 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant