browser.gpu.kernel

A GPU kernel written in heff, by combinators: an expression of the kernel is an Exp a, of a Float32, an Int32, a UInt32 or a Bool, built by the prelude’s operators (x + y, x * y, -x, x /. y of floats, x / y and x % y of integers) and this module’s functions (lit, lessThan, both, either, negation, convert, load, length); a statement is an operation of the effect stmt, so that a kernel’s body is a Co stmt Unit written with do: define, store, when, ifElse, forRange, globalId. A kernel takes its buffers, each an Input a (read) or an Output a (read and written), and is made by kernel1 to kernel3. Import it by a name, import browser.gpu.kernel as Kernel. browser.gpu.wgsl prints a kernel as WGSL; browser.gpu.run loads and dispatches it.

The kernel language has no functions, no recursion and nothing allocated: what heff computes as the body is built — a heff function called, a heff recursion, a List.map — is done then, at build time, and what is left is the kernel’s straight code, its loops and branches. The types hold what WGSL would refuse: an Exp Float32 added to an Exp Int32, a Bool added or kept in a buffer, an integer divided by /., a UInt32 negated, an Input stored into. They hold it only through these combinators: heff has no module privacy, and the constructors under them, named Unsafe... (UnsafeExp, UnsafeBuf, UnsafeKernel3), and the untyped Expr make anything.

Arithmetic is WGSL’s, not heff’s: an integer divided by zero is the dividend (heff’s is 0), and its remainder by zero 0.

BinaryOp

data BinaryOp
  = Plus
  | Minus
  | Times
  | Quotient
  | Modulo
  | Less
  | AtMost
  | Greater
  | AtLeast
  | EqualTo
  | NotEqualTo
  | AndAlso
  | OrElse

An operator of two operands, as WGSL writes it.

Expr

data Expr
  = Literal String
  | Var String
  | Binary BinaryOp Expr Expr
  | Negated Expr
  | Inverted Expr
  | Index String Expr
  | Length String
  | Convert String Expr

An expression of a kernel, untyped: a literal as WGSL writes it, a name, an operator’s application, a buffer’s element (its name and the index), a buffer’s length, a value converted to a type (its WGSL name).

Exp

data Exp t = UnsafeExp Expr

An expression of a value of the type t: of the combinators only. UnsafeExp makes one of any Expr, of any type.

exprOf

exprOf : {t : Type} -> Exp t -> Expr

The untyped expression.

Scalar

theory Scalar a where
  typeName : String
  literal : a -> String

A type a kernel has values of: its WGSL name, and a value of it as a WGSL literal. Float32’s, Int32’s, UInt32’s and Bool’s.

Numeric

theory Numeric a where
  bytes : Int

A number type of a kernel, which a buffer holds, of bytes each: Float32’s, Int32’s and UInt32’s — not Bool’s.

Signed

theory Signed a where
  signedName : String

A number type with a sign, negated by -x: Float32’s and Int32’s (WGSL has no - of a u32).

Integral

theory Integral a where
  integralName : String

An integer type, divided by / and %: Int32’s and UInt32’s.

signedLiteral

signedLiteral : String -> String

floatLiteral

floatLiteral : String -> String

int32Literal

int32Literal : Int32 -> String

instanceScalarFloat32

instance instanceScalarFloat32 : Scalar Float32

>>> instanceScalarFloat32.literal 1.5
"1.5f"
>>> instanceScalarFloat32.literal (-2.0)
"(-2.0f)"

instanceScalarInt32

instance instanceScalarInt32 : Scalar Int32

>>> instanceScalarInt32.literal (-3)
"(-3i)"

instanceScalarUInt32

instance instanceScalarUInt32 : Scalar UInt32

>>> instanceScalarUInt32.literal 7
"7u"

instanceScalarBool

instance instanceScalarBool : Scalar Bool

instanceNumericFloat32

instance instanceNumericFloat32 : Numeric Float32

instanceNumericInt32

instance instanceNumericInt32 : Numeric Int32

instanceNumericUInt32

instance instanceNumericUInt32 : Numeric UInt32

instanceSignedFloat32

instance instanceSignedFloat32 : Signed Float32

instanceSignedInt32

instance instanceSignedInt32 : Signed Int32

instanceIntegralInt32

instance instanceIntegralInt32 : Integral Int32

instanceIntegralUInt32

instance instanceIntegralUInt32 : Integral UInt32

lit

lit : {a : Type} -> {{scalar : Scalar a}} -> a -> Exp a

The value, as a literal of the kernel.

>>> exprOf (lit (2 : UInt32))
Literal "2u"

binary

binary : {a b : Type} -> BinaryOp -> Exp a -> Exp a -> Exp b

instanceAdditionExp

instance instanceAdditionExp : {a : Type}
                             -> {{numeric : Numeric a}}
                             -> Addition (Exp a)

x + y of a kernel’s numbers.

instanceSubtractionExp

instance instanceSubtractionExp : {a : Type}
                                -> {{numeric : Numeric a}}
                                -> Subtraction (Exp a)

instanceMultiplicationExp

instance instanceMultiplicationExp : {a : Type}
                                   -> {{numeric : Numeric a}}
                                   -> Multiplication (Exp a)

instanceDivisionExp

instance instanceDivisionExp : {a : Type}
                             -> {{integral : Integral a}}
                             -> Division (Exp a)

x / y of a kernel’s integers: WGSL’s, by zero the dividend.

instanceRemainderExp

instance instanceRemainderExp : {a : Type}
                              -> {{integral : Integral a}}
                              -> Remainder (Exp a)

x % y of a kernel’s integers: WGSL’s, by zero 0.

instanceFloatDivisionExpFloat32

instance instanceFloatDivisionExpFloat32 : FloatDivision (Exp Float32)

x /. y of a kernel’s floats.

instanceNegationExp

instance instanceNegationExp : {a : Type}
                             -> {{signed : Signed a}}
                             -> Negation (Exp a)

-x of a kernel’s signed numbers.

lessThan

lessThan : {a : Type} -> {{numeric : Numeric a}} -> Exp a -> Exp a -> Exp Bool

Whether the first is less than the second (<: the prelude’s is a Bool’s, not an Exp Bool’s).

atMost

atMost : {a : Type} -> {{numeric : Numeric a}} -> Exp a -> Exp a -> Exp Bool

<=.

greaterThan

greaterThan : {a : Type}
            -> {{numeric : Numeric a}}
            -> Exp a
            -> Exp a
            -> Exp Bool

>.

atLeast

atLeast : {a : Type} -> {{numeric : Numeric a}} -> Exp a -> Exp a -> Exp Bool

>=.

equalTo

equalTo : {a : Type} -> {{scalar : Scalar a}} -> Exp a -> Exp a -> Exp Bool

==.

notEqualTo

notEqualTo : {a : Type} -> {{scalar : Scalar a}} -> Exp a -> Exp a -> Exp Bool

!=.

both

both : Exp Bool -> Exp Bool -> Exp Bool

&&.

either

either : Exp Bool -> Exp Bool -> Exp Bool

||.

negation

negation : Exp Bool -> Exp Bool

!.

convert

convert : {a b : Type} -> {{to : Scalar b}} -> Exp a -> Exp b

The value as another type’s: f32(x).

Read

data Read

(A buffer the kernel reads: var<storage, read>.)

Write

data Write

(A buffer the kernel reads and writes: var<storage, read_write>.)

Buf

data Buf m a = UnsafeBuf String

A buffer of the kernel’s, of as, m how it is used: its name in the kernel. Of the combinators only (kernel1 to kernel3 name them); UnsafeBuf makes one of any name.

Input

type Input a = Buf Read a

A buffer read.

Output

type Output a = Buf Write a

A buffer read and written.

Mode

theory Mode m where
  access : String

How a buffer is used, as WGSL says it.

instanceModeRead

instance instanceModeRead : Mode Read

instanceModeWrite

instance instanceModeWrite : Mode Write

nameOf

nameOf : {m a : Type} -> Buf m a -> String

The buffer’s name in the kernel.

load

load : {m a : Type} -> Buf m a -> Exp UInt32 -> Exp a

The buffer’s element at the index.

length

length : {m a : Type} -> Buf m a -> Exp UInt32

How many elements the buffer has.

StmtF

data StmtF (m : Type -> Type) x
  = Let Expr (Expr -> x)
  | Store String Expr Expr (Unit -> x)
  | If Expr (m Unit) (m Unit) (Unit -> x)
  | For Expr Expr (Expr -> m Unit) (Unit -> x)
  | GlobalId (Expr -> x)

A statement of a kernel, untyped: a value named (the name to the rest), an element of a buffer written (the buffer’s name, the index, the value), a branch (each side’s statements), a loop from the first up to the second (its body given the counter), and the invocation’s index in the grid (named, to the rest).

stmtMap

stmtMap : {m : Type -> Type}
        -> {a b : Type}
        -> (a -> b)
        -> StmtF m a
        -> StmtF m b

stmtThrough

stmtThrough : {m : Type -> Type}
            -> {n : Type -> Type}
            -> ({x : Type} -> m x -> n x)
            -> {a : Type}
            -> StmtF m a
            -> StmtF n a

stmt

stmt : HFunctor

For a kernel’s body: values bound, stored in a buffer, branches and loops, and which invocation this is — what the kernel’s WGSL is written from.

define

define : {a : Type} -> Exp a -> Co stmt (Exp a)

The value named, once: the name, to use it again where it is computed once (let v0 = ...;).

store

store : {a : Type} -> Buf Write a -> Exp UInt32 -> Exp a -> Co stmt Unit

The buffer’s element at the index written: only a buffer the kernel writes, an Output.

ifElse

ifElse : Exp Bool -> Co stmt Unit -> Co stmt Unit -> Co stmt Unit

The first statements where the condition holds, else the second.

when

when : Exp Bool -> Co stmt Unit -> Co stmt Unit

The statements where the condition holds.

forRange

forRange : {a : Type}
         -> {{integral : Integral a}}
         -> Exp a
         -> Exp a
         -> (Exp a -> Co stmt Unit)
         -> Co stmt Unit

The body for each integer from the first up to the second, not it.

globalId

globalId : Co stmt (Exp UInt32)

The invocation’s index in the grid, along its first axis: from 0 to the workgroups dispatched times the workgroup’s size, less one.

Param

type Param = { name : String, access : String, element : String }

A buffer of a kernel, as WGSL declares it: its name, how it is used (read, read_write), the type of its elements.

Kernel

type Kernel =
  { entry : String, workgroup : Int, params : List Param, body : Co stmt Unit }

A kernel, untyped: the name of its entry point, its workgroup’s size, its buffers in the order they are bound, its body.

Parameter

theory Parameter p where
  declared : String -> Param
  named : String -> p

What a kernel takes: a buffer, of numbers, read or written.

instanceParameterBuf

instance instanceParameterBuf : {m a : Type}
                              -> {{mode : Mode m}}
                              -> {{scalar : Scalar a}}
                              -> {{numeric : Numeric a}}
                              -> Parameter (Buf m a)

Kernel1

data Kernel1 a = UnsafeKernel1 Kernel

A kernel of one buffer, an Input a or an Output a. Of kernel1 only; UnsafeKernel1 makes one of any Kernel.

Kernel2

data Kernel2 a b = UnsafeKernel2 Kernel

… of two.

Kernel3

data Kernel3 a b c = UnsafeKernel3 Kernel

… of three.

kernel1

kernel1 : {a : Type}
        -> {{pa : Parameter a}}
        -> String
        -> Int
        -> (a -> Co stmt Unit)
        -> Kernel1 a

A kernel of the entry point’s name and the workgroup’s size, its body given its buffer (named a).

kernel2

kernel2 : {a b : Type}
        -> {{pa : Parameter a}}
        -> {{pb : Parameter b}}
        -> String
        -> Int
        -> (a -> b -> Co stmt Unit)
        -> Kernel2 a b

… its body given its two buffers (a, b, bound in that order).

kernel3

kernel3 : {a b c : Type}
        -> {{pa : Parameter a}}
        -> {{pb : Parameter b}}
        -> {{pc : Parameter c}}
        -> String
        -> Int
        -> (a -> b -> c -> Co stmt Unit)
        -> Kernel3 a b c

… its body given its three buffers (a, b, c).

kernelOf1

kernelOf1 : {a : Type} -> Kernel1 a -> Kernel

The kernel, untyped.

kernelOf2

kernelOf2 : {a b : Type} -> Kernel2 a b -> Kernel

kernelOf3

kernelOf3 : {a b c : Type} -> Kernel3 a b c -> Kernel