Safe Haskell	Safe-Inferred
Language	Haskell2010

PlutusCore.Unroll

Contents

Peano numbers
Statically unrolled list drop
Statically unrolled effectful iteration

Description

Static loop unrolling utilities using type-level Peano numbers.

This module provides utilities for statically unrolling loops at compile time. GHC resolves the type class instances at compile time, resulting in unrolled code that avoids runtime overhead.

See Note [Static loop unrolling] for details on the technique.

Synopsis

data Peano
- = Z
- | S Peano
type family NatToPeano (n ∷ Nat) ∷ Peano where ...
class Drop (n ∷ Peano) where
- drop' ∷ [a] → Maybe [a]
dropN ∷ ∀ n a. Drop (NatToPeano n) ⇒ [a] → Maybe [a]
class Applicative f ⇒ UpwardsM f n where
- upwardsM ∷ Int → (Int → f ()) → f ()

Peano numbers

data Peano Source #

Peano representation of natural numbers for type-level recursion.

Constructors

Z
S Peano

type family NatToPeano (n ∷ Nat) ∷ Peano where ... Source #

Convert a type-level Nat to Peano form for instance resolution.

Equations

NatToPeano 0 = 'Z
NatToPeano n = 'S (NatToPeano (n - 1))

Statically unrolled list drop

class Drop (n ∷ Peano) where Source #

Statically unrolled drop: drops exactly n elements if possible. Returns Nothing if the list has fewer than n elements.

The n parameter is a Peano number that guides instance resolution. Use dropN for a more convenient interface with Nat literals.

Methods

drop' ∷ [a] → Maybe [a] Source #

Instances

Instances details

Drop 'Z Source #
Instance details Defined in PlutusCore.Unroll Methods drop' ∷ [a] → Maybe [a] Source #
Drop n ⇒ Drop ('S n) Source #
Instance details Defined in PlutusCore.Unroll Methods drop' ∷ [a] → Maybe [a] Source #

dropN ∷ ∀ n a. Drop (NatToPeano n) ⇒ [a] → Maybe [a] Source #

Drop exactly n elements from a list, returning Nothing if too short.

The drop count is statically unrolled at compile time via instance resolution.

dropN @3 [1,2,3,4,5] == Just [4,5]
dropN @3 [1,2]       == Nothing

Statically unrolled effectful iteration

class Applicative f ⇒ UpwardsM f n where Source #

Statically unrolled effectful iteration over a range.

upwardsM i k means k i *> k (i + 1) *> ... *> k (i + n - 1).

We use this to statically unroll loops through instance resolution. This makes validation benchmarks a couple of percent faster.

Methods

upwardsM ∷ Int → (Int → f ()) → f () Source #

Instances

Instances details

Applicative f ⇒ UpwardsM f 'Z Source #
Instance details Defined in PlutusCore.Unroll Methods upwardsM ∷ Int → (Int → f ()) → f () Source #
UpwardsM f n ⇒ UpwardsM f ('S n) Source #
Instance details Defined in PlutusCore.Unroll Methods upwardsM ∷ Int → (Int → f ()) → f () Source #