effectfully

In this post we'll tell a story of how we got a 12% performance improvement in our production evaluator.

I looked into GHC Core of the production evaluator and spotted this there:

case safeIndexOne env1_XW (W64# bx18_scPRb) of {
  Nothing -> jump exit_X16 <...>
  Just val_acLQA -> jump returnCek_scPkh ctx1_X0 val_acLQA <...>
}

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE DeriveFoldable #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE StandaloneDeriving #-}

	module H6IndexedFolds (module H6IndexedFolds) where

	module IsMatching where

	import Data.Function
	import Data.List
	import Data.Maybe

	getSubterms :: (Integer -> Integer -> [Integer]) -> [Integer] -> Maybe (Integer, Integer)
	getSubterms f xs =
	let subtermIndices =
	map (snd . head) . groupBy ((==) `on` fst) . sortBy (compare `on` fst) . catMaybes $

	{-# OPTIONS_GHC -Wall #-}

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE KindSignatures #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE ScopedTypeVariables #-}

	{-# LANGUAGE ConstraintKinds #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE KindSignatures #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE UndecidableInstances #-}

	{-# OPTIONS --type-in-type #-}

	open import Function
	open import Relation.Binary.PropositionalEquality
	open import Data.Unit.Base
	open import Data.Empty
	open import Data.Product
	open import Data.Nat.Base

	{-# NO_POSITIVITY_CHECK #-}

	{-# OPTIONS --type-in-type #-}
	{-# OPTIONS --no-positivity-check #-}
	{-# OPTIONS --no-termination-check #-}

	-- Agda obviously doesn't have self-types, so we fake them here.
	postulate
	ι : {A : Set} -> (A -> Set) -> Set
	gen : {A : Set} {B : A -> Set} -> ∀ x -> B x -> ι B
	inst : {A : Set} {B : A -> Set} -> ∀ x -> ι B -> B x