---
title: Call 2023-03-22
tags: S+S, Semantics
---

# GHC

## Threshold arity (#23113)

* `threshold_arity` (in `dmdAnalRhsSig`)
* For join points may be less than the `idArity` (or I suppose greater than if we for some reason the `idArity` is totally out bogus).
* For non-join points is equal to `idArity` (see `thresholdArity`).
* In `dmdAnalRhsSig`, the `final_rhs_dmds` will be at least as long as the `threshold_arity`. For join points it could be longer if `let_dmd` had a lot of call demands.

  join j x = blah in e

in a context of `C(C(C(Top)))`.
* So in `splitFun`
* For join points, the length of `wrap_dmds` may be
* less that `idArity`. e.g.

      join j x = \pqr. blah in ...(jump j 1)... (jump j 2)...

Here idArity is 4, but join-arity is 1.
* more han `idArity`. eg

      f (join j x = blah in e)

where `f` has a demand `C(C(C(Top)))` on its arg.
* For non-join-points, should be equal.

Care with:
* `take threshold_arity` in finaliseArgBoxities. Why?
* `mkDmdSigForArity`
* Why do this at all?
* When trimming, we keep the same `div`; looks wrong.

Reason for trimming. Worker-wrapper is driven by dmd sig; and w/w makes wrapper have arity N where N=length wrap_dmds; in effect, does eta-expansion.

f (join j x = blah in e)
-- where f has a C1(C1(top)) demand on it its arg

Then it would be OK to eta expand and w/w to

f (let $wj x' p q' = let x = I# x'; q = I# q' in blah
   in join j x = \ p q. case x of I# x' -> 
                          case q of I# q' -> $wj x' p q'

Semantically sound, but $wj is not a join point -- bad.

Conclusion: length `wrap_dmds` = threshold_arity, including for join points. So that we w/w for threshold_arity.

f x y = x+y
Analyse with C(CS(top))
DmdTy [strict, strict] top
Trim in mkDmdSigFor Arity
DmdTy [strict] top
seems wrong.

But maybe not-wrong for join points??

f (join $wj x' p q = let x = I# x'; q = I# q' in blah
   in join j x = \ p q. case x of I# x' -> 
                 jump $wj x' p q

## Eta expansion of arguments (#23083)

https://gitlab.haskell.org/ghc/ghc/-/merge_requests/10088

* Note [No crap in eta-expanded code] and Note [Eta expansion for join points] ==> don't eta expand join point heads in Prep
* `case patError @() of {}` lowering to ``patError @() `cast` co :: () ~ Int# -> Int#`` and `mightBeFunTy` guessing in the Backend
* Seems to be a general problem of -XEmptyCase lowering.

f :: Bool -> Int# -> Int#
f True = patError @() of {}
f False = \x. x

CorePrep:

f :: Bool -> Int# -> Int#
f True = patError @() `cast` co :: () ~ Int# -> Int#
f False = \x. x

eta:

f :: Bool -> Int# -> Int#
f True eta = (patError @() `cast` co :: () ~ Int# -> Int#) eta
f False eta = eta

and that does trigger an assertion on line 1031 of StgToCmm.Expr

        EnterIt -> assert (null args) $  -- Discarding arguments
                   emitEnter fun

## (#23145)

https://gitlab.haskell.org/ghc/ghc/-/merge_requests/10152

# Semantics

http://siek.blogspot.com/2017/06/revisiting-well-typed-programs-cannot.html

## Introduction

* Move Related Work to Related Work
* Is divergence really that important to people?
* Bring simple usage analysis (perhaps *instead* of absence anlsyis, or recovering latter as special case)

## Maximality

Non-retreating trace that is maximal

## Domain Theory

Thinking a lot about Domain Theory.
Continuity of S proves challenging withtout baking maximality of traces (or bot) into the domain

## Stateless semantics

Working on stepwise abstraction to stateful semantics

# Discussion

**Balanced** = first two bullets

A balanced trace can end up with a state that is deeper than k1. Maybe "non-retreating".

**Maximally balanced** = pi is balanced and either pi is infinite or (if pi is finite) there is no sigma' st (pi:sigma') is balanced.

SG: **claim**: for any finite, non-stuck maximally balanced trace, final stack is k1. Of course you have to define "non-stuck".

S[[e]] (e, env, heap, k)
map (add k) (S[[e]] (e,env, heap, []))

S[[e]] (env, heap) = ...