Zilch1-2-3 features preview

[Mesabloo]

One of the main goals of Zilch is to reduce the amount of undefined behaviors through type safety.
However, some features also provide quality of life when using the language itself.

Notation used for the remaining of this post:

• 🔥 marks an undefined behavior-beating feature
• ✨ simply describes quality of life improvements for the language
• 💡 are some ideas that need to be truly accepted or rejected
• 🔑 for some features which are essential

---

This list might get modified at some point, depending on how the language evolves. This is the current state for Zilch:

• 🔥 Safe memory handling¹ through either:
  • Linear/Affine types
  • Regions (with capabilities? see the calculus of capabilities)
  • An area system much like regions
  • Quantitative types (see dependent types)
  • Reference capabilities (see Introduce reference capabilities in Zilch #6)
  • (Explicit?) Region-based memory management (to deal with the ω multiplicity of QTT)
• ✨ Row polymorphism with anonymous records and polyvariants
• 🔑 GADTs and records
• ✨ Safe ad-hoc polymorphism using typeclasses and implementations
• 🔥 Safe effectful expression handling with algebraic effects (see Add algebraic effects to Zilch #7)
• 🔑 Distinguish boxed from unboxed types (e.g. u64 vs *u64 or &u64; some types may be boxed by default without explicit markers)
• 🔥 Dependent types (integrates well with quantitative types)
• ✨ C-targeting FFI (effectful computations need to be encapsulated on the Zilch side)
• 💡 Some specific kind of bitfields
• ✨ Explicit thunks
• 💡 Static (compile-time) contracts
• ✨ Mixfix operators
• ✨ Rank-N types (this one might come naturally with dependent types)
• 💡 Universe polymorphism
• ✨ Implicit arguments

---

Note: all of these features are the currently planned ones for the first two versions of Zilch. The second version of Zilch (and in fact, the first version also²) should be completely bootstrapped from the original, minimal Zilch compiler written in Haskell.

---

¹: Problems arise when using any other kind of "resource" than memory (files, sockets, shared memory, ...) for all alternatives proposed other than linear/affine types and reference capabilities.

²: The first version of the compiler will firstly be written in Haskell, then fully rewritten in Zilch. This will take time, but as we do not add any feature whatsoever during this process, the major version should not be changed (according to semantic versioning).

[Mesabloo]

Feature discarded.

This does not seem to integrate that well with the rest of the language, and also increases a lot the overhead on the programmer.

[Mesabloo]

Algebraic effects seem like a nice addition to the language, in order to be explicit about side effects of a given function.

• Haskell (and some other functional programming languages) uses monad to show those inside function types (e.g. main :: IO ()), but this has the disadvantage to need a rather big amount of boilerplate code: composing multiple monads (e.g. State s with Except e) is achieved using monad transformers, which require extra typeclasses/instances, manual unfolding of monads, etc.
• OCaml uses exceptions, which are not modeled into the type system, and do not model side effects such as console output

Algebraic effects generalize exceptions by allowing arbitrary computation-stopping (potentially resuming) functions to be called. Effects are also present in the type system, disallowing not handling some effects when required, or being effect-polymorphic.

---

Here is how the language can be extended for effects:

• Add a construct to declare effects, e.g.

  effect <name>(<id>...) :=
    <op₁> : <type>
    <op₂> : <type>
    ⋯
    <opₙ> : <type>
  

  where each opᵢ is a way to “trigger” the effect handler for the declared effect, and must be unique across all effects
• Allow creating handlers using a specific handle construct:

  • try <expr> with { <op₁> → <ex₁> ; <op₂> → <ex₂> ; ⋯ ; <opₙ> → <exₙ> ; return <id> → <exᵣ> } handles any effect that evaluating expr can have, going to the branch return ... → ... when no effect has been “thrown” (this might be extended in the same way as the Haskell language extension -XLambdaCase)

    When handling an effect, we have to handle all possible effects (but we may only handle one effect at a time)

• Only functions can be effectful, where the return type of an arrow can be augmented with an effect row (no row means that a computation is pure)
  Grammar still needs to be fixed in order not to clash with reference capabilities

Foreign imported C functions cannot be made effectful, in order not to expose the internal effect handler API.
Specific ways of importing can be included in the language in order to somehow force adding effects to foreign functions by wrapping them in effect-triggering functions.

[Mesabloo]

Reading around at the koka website, there are many things changing from the first published paper.
Our with “statement” is directly inspired by Koka's, as well as most of our effect operations. However, Koka also has an handler construct, which mostly equates binding all operations using with and simply calling the action at the end of the scope. This is basically syntactic sugar, therefore quality of life, but will not be considered for the first version of Zilch (which should be quickly superseded by the second version, after the whole rewrite of the compiler).

I believe that the handle ... with ... construct is not really needed (which frees the 2 reserved words return and handle), as we can just scope the expression with with effect bindings.

As for the grammar change described just on the comment above, there are multiple ways to handle this:

• specify the type of let bound functions with -> for the return type, which can be prefixed by a row of effects
• allow writing ... -> effect-row return-type as in Koka (where effect-row is one of an identifier or a <> delimited basic row). This approach is a bit more ambiguous, considering the capabilities' grammar capability type
• reserve a special operator to indicate effects, e.g. ... -> return-type & effect-row. The only downside of this is that we either have to reuse an already-reserved operator (and there aren't many) or reserve a new operator just for this purpose (the best fitting would be &, + or #)

The third option is, I believe, the better one as it does not require use to change the grammar of lets, and it doesn't clash with capabilities (plus & is easily read and not so intrusive in source code¹).

---

⁽¹⁾:

let id_log<a, e | show(a)>(x : a) : a & <console | e> :=
  let () = print(x) in
  x

effect state(s) :=
  get : () -> ref s
  put : forall<c | c <: val> () -> c s

let state<a, b, e>(init : a, action : () -> b & <state(a) | e>) : b & e :=
  -- assuming a module imported qualified as `box`
  let st : lin box(a) := box.new(init) in
  box.asref(st, st ->  -- we need `st` to be a `ref` instead of a `lin`
    with get() := box.deref(st)
    with put(s) := let () = box.set(st, s) in resume() in

    action())

[Mesabloo]

Koka also allows using functions already defined in the with construct, used like with <funcall> which brings the handler as the default handler for the consumed effect (this can be found while inspecting the type of the function reference, which must be of the form forall<b, e> (() -> b & <x | e>) -> b & e, where x is any given effect which must be handled.

This specific constructs makes it possible to define generic handlers which may themselves be parameterized.

[Mesabloo]

With the recent removal of refcaps, the syntax for effectful computations can be simplified a little bit.
The idea is to use the same notation as in Koka, i.e. (parameters...) -> effects return-type, where effects is any of:

• a simple identifier (potentially applied to some parameters) corresponding to a defined (and in-scope) effect
• the combination of multiple effects, written <effect1, effect2, ..., effectN>
• a variable whose type is effect
• an extended row of effects, written <effect1, ..., effectN | vars...> where vars are comma-separated variables of type effect

The above example can therefore be rewritten as:

effect state(0 s : type 0) ≔
  val get : () → s
  val put : (1 _ : s) → s

-- state : ∀{0 s : type 0, 0 b : type 0, 0 e : effect}.
--           (1 init : s, 1 action : () → <state(s) | e> b) → e b
let state {0 s} {0 b} {0 e} (1 init : s) (1 action : () → <state(s) | e> b) : e b ≔
  local-mut λ () →
    let st : box(s) ≔ box.new(init)

    with get() ≔ resume(* st)
    with put(s) ≔ st ← s ; resume()

    action()

Note that because of the lack of explicit multiplicity, st is considered unrestricted (this will be described later in a more in-depth description of the QTT).

[Mesabloo]

The syntax shown earlier uses multiple with bindings.
Let us consider this quick example:

effect console :=
  puts : (1 _ : c-string) -> ()
  gets : () -> c-string

#[import "puts"]
val c-puts : (1 _ : c-string) -> ()

let console-handler {0 a} {0 e} (1 action : () -> <console | e> a) : e a :=
  with puts := c-puts
  with gets := ?todo
  action ()

In the body of console-handler, there is no information regarding whether the two with statements cover the same effect or not.
There are two solutions to this:

• we can prefix every effect handler with the name of the effect (e.g. with console::puts := ?)
• we can bind every method of an effect in the same with statements (e.g. with { puts := c-puts ; gets := ?todo })

The first one works but does not seem easy to implement: how does one detect/report an error about an incompletely handled effect?
The second one, on the other hand, seems a little less consistent regarding the other parts of the language (see scoped enums and records), but is way easier to detect (in the case where multiple effects with the same handlers' names cannot be defined).

[Mesabloo]

The problem above can be solved using the following syntax:

let console-handler {0 a} {0 e} (1 action : () -> <console | e> a) : e a :=
  with console
    let puts := c-puts
    let gets := ?todo
  action ()

That way, it also allows us to specify whether the handler is recursive or not (whatever it may mean, we could not support that at all).

We can therefore easily detect if we handled all the effects, and it is also clear which we are trying to handle (console may also be qualified identifier).

[Mesabloo]

Feature discarded for now.

Not completely sure if this will come back in the language at some point (maybe later once the basis is laid).
But for now, it won't.

[Mesabloo]

There are multiple ways to handle ad-hoc polymorphism (re-defining a given function with different types):

1. Going for the “C++ way”, where ad-hoc polymorphism is unrestricted and difficult to type. This also makes type errors harder to show, and type inference much harder to implement.
2. Going for the “Haskell way”, where ad-hoc polymorphism is managed through the use of type classes and class implementations. This makes type-checking a bit easier than the first approach, but still complicates things quite a bit.
3. Simply no ad-hoc polymorphism, which is not very satisfactory.

The retained option is number 2, adding type classes and implementations.
For this to work, we have to think about:

1. type constraints:
   • we have to have a constraint kind representing any concrete (fully applied) constraint.
   • ∀-quantified variables can be restricted to only have implementations for specific implementations (taking in account the -XFlexibleConstraints extension of Haskell).
   • a constraint is considered ambiguous if any of its type variable arguments is left unused in the function type, e.g. forall<a | show(a)> u64 -> u64
2. type classes:
   • type class defiinitions can only contain type variables in their heads, and reference those inside the members' types.
3. type class implementations:
   • type class implementations are unrestricted (taking the -XFlexibleInstances, -XMultiParamTypeClasses and some other Haskell extensions as default) and also allow using a special _ (or ·) as a sort of a “function hole” (like at the expression level). This is sufficiently restricted not to need higher order unification of type terms (which would be undecidable).

[Mesabloo]

explicitly passing an implementation dictionary when calling a function

We can have a dedicated syntax, e.g. {dict1 := dict2}, for explicit dictionary passing binding the constraint dict1 to dict2. We could even go even further and have a full-on record which is used to pass all constraints dictionaries (not accounting for default implementations, if not specified).
We could then write some_func<{eq := string_eq_case_insensitive}>(some_argument), which could be simplified to func<{string_eq_case_insensitive}>(some_argument) because constraints are also determined on the order they appear in (the first notation is useful when partially specifying constraints).

explicitly using an implementation dictionary among the ones passed as constraints in a function definition

Every constraint can be named in a forall quantifier. This brings the dictionary (may it be infered or not) into the type and expressions scopes (allowing to use functions from specific dictionaries; if unnamed, the dictionary is implicitly opened), and also allows multiple "same" constraints to be bound in the same type (in which case names are necessary), e.g. forall<a | eq1 : show(a), eq2 : show(a)> ... (which implies that eq1.(==) and eq2.(==) may be different functions).

This only causes problems for type class members, where the constraint generated (for the class itself) has no name real usable name¹.
We might solve this problem by allowing type classes (and their constraints) to be also named, however the problem really arises if we have a class head like class X(a) | X(a) := ..., which can explicitly be disallowed because it creates an infinite cycle (having a class depend on an instance of itself with the same arguments).

Constraints with the same name could also be implicitly passed to further function calls, making it so that we don't need to explicitly pass those dictionaries as {dict := dict} for each subsequent call (in the same manner as implicit parameters in Haskell).

---

⁽¹⁾

class X(a) :=
  f : a -> a -> a

=>

f : forall<a | __c2255351 : X(a)> a -> a -> a

(2255351 is a random generated number by the typechecker)

[Mesabloo]

Minor syntax change: members of typeclasses are now prefixed with val, which allows operators to be declared with fixities (this was a limitation found earlier).

Before, one would have had to do

class C(a1, a2, ..., an) :=
  name : type
  
#[fixity]
let (op) := name

Thanks to the new syntax, it is now possible to do

class C(a1, a2, ..., an) :=
  #[fixity]
  val (op) : type

while keeping a consistent grammar (the same applies for records and enums, which will be described in another reply).

[Mesabloo]

There is no need for a specific class construct.
We can make use of implicit parameters using records with no associated constructor.

However, some issues arise when doing so:

1. Ideally, type classes are “invisible”, meaning that we can use their members unqualified and the instance record (the qualification) is automagically determined.
2. Implicit parameters are not automatically propagated by name at call sites. This is a behavior wanted for instances.

Point 1 can be addressed by “creating” a new construct as in Agda (see here), where records can be publicly opened using open MyRecord {{...}} public (the accessor can be changed if needed) at the top-level.
This approach can be adapted to only allow constructor-less record to be opened at the top-level, as they would fulfill the constraints.

Point 2 is addressed in Agda by creating a new syntax with {{ }} which automatically infers what instance record to use (and propagates them by name).
This same idea can be used to infer and propagate instance records while opening them in the current scope.
Note that this is not fully required, as the syntax {open _ : record} can be used in place of {{_ : record}} but it does not allow propagating names.

[Mesabloo]

The open Type {{...}} syntax (can be shortened to open Type or open Type {{}} if needed, but this is to be discussed) may also be used to "open" data-types, meaning putting their constructors into scope (data constructors are scoped by default).
This construct may be used both at the top-level of a file, or inside an expression.

Examples include:

record X :=
  x : c-string
  y : u64
  
open X {{...}}

-- here:
-- x : X -> c-string
-- y : X -> u64

data Maybe (0 a : type 0) :=
  just : {_ a} -> 1 a -> Maybe a
  nothing : {_ a} -> Maybe a
  
let safe-div (1 x : s64) (y : s64) : Maybe s64 :=
  open Maybe {{...}}
  if y = 0 then nothing else just (x /# y)
  -- normally, this would have been:
  -- if y = 0 then Maybe::nothing else Maybe::just (x /# y)

Note that, when used at the top-level, the constructors/fields can be exported directly by the module.

[Mesabloo]

The syntax might as well be revised to open {{Type}} for several reasons:

• this does not introduce the semi-reserved symbol ...
• this reuses the reserved {{ and }} (unicode ⦃ and ⦄) which are used to pass implementation records
• because records and data-types have constructors/fields which are scoped inside them, reusing {{ and }} makes sense (remember that {{_ : Type}} automatically opens the implementation record in the scope)
• open Type {{}} is simply ugly and confusing (what do the {{}} mean?)

[Mesabloo]

A Foreign Function Interface (FFI) is a powerful mechanism which can be used to interact with code written in other languages.
Most modern programming languages feature those, as it allows using e.g. the complete libc instead of reimplementing everything from scratch.
However, types must be represented the same for this to work.
For example, if a C function accepts a struct { int x; char c; }, then the function on the Zilch side must accept a type with the same size (padding taken in account). Ideally, this type is also a record, but it is in fact not required, as this cannot be checked at all.

Also, some of the considered features (e.g. effects) cannot be exposed to the C side at all, without exposing the complete internal ABI.
Therefore, foreign functions cannot be effectful on the Zilch side.
Also, because of the nature of foreign functions (i.e. they are highly unsafe), they will not be allowed to be exported by modules, needing to be wrapped on the Zilch side.
Some optimisations can later be performed in order to remove the level of indirection added by aliasing those foreign functions.

The proposed syntax for foreign imports and exports is:

• #[import "optional header" identifier1] val identifier2 : type to import the function identifier1 under the name identifier2 with the type type. Note that a header name can also be specified while importing functions if needed.
• #[export] let ... tries to export the function defined without changing its name (some restrictions may apply to its type).

The ABI used by types will need to be deeply documented.
Some types (e.g. dependent types) will most likely be very hard to use with the FFI (at least safely) but this will be tackled in time.

[Mesabloo]

Got to realise that the header name is actually useless when not compiling to C.
The function is actually imported when linking all the code together. And headers do not exist anymore when linking.

Also, we might want to be able to import functions with disallowed names (for example functions with _ inside), and also different calling conventions.
The syntax therefore evolves into #[import ccall "identifier1"] val identifier2 : type where ccall is the default if unspecified.
The standard defined calling conventions only contain ccall, but more may be added when implementing a Zilch compiler (e.g. for the Java Virtual Machine or the .NET environement).

[Mesabloo]

Mixfix operators allow customizing the grammar of Zilch expressions (understand values and types) by indicating how some expressions may be syntactically formed.
For example, declaring an operator _≡_ is the same as dynamically producing the grammar rule expr '≡' expr, where each _ (called a mixfix hole) is replaced with a grammar rule accepting any expression.

These kinds of operators never made it into mainstream programming languages (only a few programming languages support these, e.g. Agda or Coq) because of how complex they are to parse (ambiguities happen very quickly: which if_then_else_ takes the last else in the example if t then if u then v else w? Most implementations would yield grammar ambiguities with both ways to parse this input).

There are 4 kinds of mixfix operators:

• prefix operators, ending with a hole (e.g. -_, ¬_)
• infix operators, starting and ending with holes (e.g. _-<_>-_, _+_)
• postfix operators, starting with a hole (e.g. _!, _cm)
• closed operators, not starting nor ending with holes (e.g. {{_}}, <_,_>)

Ambiguities really come from mixing prefix, postfix and infix operators (closed operators do not have ambiguity problems).

Every hole in a mixfix operator declaration should be separated by a non-reserved non-blank word. For example, _ _ is not accepted (some languages accept it as the function application operation, but it creates a lot of syntactical ambiguities and is better off inside the minimal grammar) and _ also isn't (because it would match with everything, yielding both syntactical ambiguities and unnecessary function applications). Be aware of <_, _> which is not valid because of the unwanted whitespace in the middle.

[Mesabloo]

GADTs and records allow structuring data in specific “or” branches or “and” groups.
GADTs (short for Generalized Abstract Data Types) are more expressive forms of ADTs which allow for various type constraints to be expressed on the "cases" instead of the global data type.
Records appear in two variants:

• constructor-less records, analogous to typeclasses in Haskell, which cannot be explicitly constructed
• “normal” records with a given constructor

---

GADTs can be declared using the data syntax as in the example:

data Maybe {l : Level} (a : type l) :=
  val just : a -> Maybe a
  val nothing : Maybe a

Records can be declared using the syntax in this example:

record tuple-2 {l : Level} (a b : type l) :=
  constructor _×_
  val fst : a
  val snd : b

Note that constructor is a keyword only inside the top-level of a record declaration, else it works as a normal identifier.
The constructor statement can be ignored, but it must be placed at the beginning if it appears.
Also note that the constructor will be given N arguments, where N is the number of fields in the record, so if the constructor is a mixfix operator, it must have N holes _.

---

Both GADTs and records can be pattern matched on, using the match_with_ construct.
GADTs are pattern matched on each of their “branches” (identified by their names in the declaration) while records are pattern matched on their constructors (or opened).
Please note that pattern matchings must be exhaustive, else a compile-time error will be thrown.

[Mesabloo]

There are a few cases where lazy evaluation is needed, e.g. to define custom control structures.
One example of such whould be

let if_then_else_ {0 l} {0 α : type l} {0 ε : effect} (1 cond : bool) (t : lazy α ε) (e : lazy α ε) : ε α :=
  match cond with
    true  -> t
    false -> e

Note: This example is better off as a builtin structure or compiled to efficient code (in fact, many control structures are better off compiled to efficient code).

In some programming languages with first-class support for lambda expressions, people tend to use nullary functions to express "to be executed" computations.
Some other, e.g. Kotlin or Koka, even provide syntactic sugar for those in order to make them very readable (f { ... } instead of f(() -> ...)).

There are 3 alternatives which can be considered:

1. Do not make use of thunks (unevaluated expressions), and use the type type lazy α ε := unit -> ε α to represent lazy values. This works but does not provide free memoization of pure lazy values (evaluation is forced to NF every time the function is called).
2. Explicit thunks with builtin construct to force evaluation/construct a thunk. This closely relates to CBPV (Call By Push Value). That way, thunk { e } represents the unevaluated expression e, and force t (or eval t) evaluates the thunk to WHNF, while memoizing the result if pure (memoizing an impure result has side-effects that we might want to investigate before making a definite choice about this point).
3. Fully implicit thunks, using a builtin lazy type which would represent thunks (as in Idris). However, because the language itself isn't fully lazy by default (as opposed to Haskell), this makes things a bit harder to determine when to evaluate a thunk/"thunkify" an expression statically (we may be able to do this dynamically, but I believe this would make performance way less predictable).

[Mesabloo]

Implicit parameters augment the language with inference extension to automatically determine some function/data/record parameters.
This is particularly useful to propagate type information without explicit user annotations.

In Zilch, they are specified using the {mult id : type} syntax, and must always be placed before explicit parameters (let f {a} {b} (c) (d) := ... is valid while let f {a} (c) (d) {b} := ... is not).

The compiler then treats them as placeholders which must be statically resolved without requiring user input (failure to do so yields a compile-time error about an unresolvable implicit argument).
However, it is sometimes needed to explicitly bind implicit parameters. This is done using the syntax {...} at the call site, just like a regular function call argument.
Restrictions apply on the order parameters appear in: if the second implicit argument of a function f needs to be given, it is required to bind the first the first to the explicitly-infered anonymous argument {_}, yielding the call f {_} {something} ....
The function call f a b c is semantically equivalent to f {_} ... {_} a b c when f has implicit arguments (in fact, the compiler is allowed to do such transformation without user consent, as it does not change static semantics).

If the implicit argument is of a record type, it can also be opened by prefixing the identifier with open (i.e. {open my-record : of-some-type}).

[Mesabloo]

An improvement over "normal" modern low-level programming languages is the use of "quantities" (or "usages") to specify the compile-time/runtime of some expressions.
There are a few kinds of usages:

• 0 is the usage of erased, compile-time expressions. Such expression does not exist at runtime.
• 1 is the usage of linear, runtime expressions. Note that a linear value must be used only once inside an expression. For example, the function let dup{0 A}(1 x : A) ≔ 〈 x , x 〉 cannot be typed when x is linear.
• ω means that an argument can appear any number of times in any position (compile-time or runtime). This is essentially an unrestricted value. However, beware that these unrestricted expressions will always have runtime presence, even if only used at compile-time.

A great addition to such system is "usage polymorphism", meaning that some values can have an "unknown" usage at declaration site, which will thereby be monomorphised (or not, up to the implementation) at call-site. This idea is present in Frank, although its type system is actually linear, not quantitative.
A way to achieve this would be for example the following usage-polymorphic identity function:

let id{0 k, 0 A}(k x : A) ≔ x

Here, k : usage and A : type, which means that id has type {0 k : usage, 0 A : type} → (k x : A) → A (I am not quite sure yet if we need to qualify the return type A with the usage k or not. If yes, then we'll also need a syntax for that, as k A is rather ambiguous and ugly).

Usage-variables will always need to be qualified with a 0 usage (and this must be enforced by the implementation when type-checking).
Moreover, having usage : usage does not seem to break soundness at first glance, though this should be investigated more thoroughly in order to prove that.

[Mesabloo]

Adaptating the linear type system described in Treloar's thesis (see #11 (comment)) does not seem to be as cumbersome as it seems.
The only real issue is to accomodate for the 0 usage.

As an example, let us define the ⩽ relation on usages¹, where ρ ⩽ π means that π is less permissive than ρ (this can also be read as "we can use a value with ρ usage as if it was a π usage in typing rules):

 ρ ∈ {0, 1, ω}         ρ ∈ {0, 1}
---------------       ------------      -------
     ω ⩽ ρ               1 ⩽ ρ          0 ⩽ 0

This allows to derive the following typing rule (where Γ ⊢ x ⇒ⁱ A means that x can be infered to have type A with usage i using the context Γ (which is left undefined for now), Γ ⊢ x ⇐ⁱ A means that A can be checked to be of type A with usage i using the context Γ, and A ≅ B means that A and B are computationally equivalent) for implicit type and usage conversion²:

 Γ ⊢ e ⇒ⁱ A     A ≅ B     i ⩽ n
---------------------------------- [ᴛʏᴘᴇ-ᴄᴏɴᴠ]
            Γ ⊢ e ⇐ⁿ B

This reads as "e can be checked to have type B with usage n iff e can be infered type A with usage i, A and B are computationally equivalent (they are merely the same type) and the usage i is more permissive than the usage n".

Other typing rules may as well be easily defined in the QTT setting (most probably reusing those already added in the current type-checker -- see for example

zilch/lib/gzc-typechecker/src/Language/Zilch/Typecheck/Checker.hs

Lines 83 to 87 in 35fe998

	{-
	0Γ ⊢ (y :^π A) → B ⇐^0 type ℓ Γ, x :^σπ A ⊢ e ⇐^σ B
	─────────────────────────────────────────────────────────────
	Γ ⊢ λ(x :^π A) → e ⇐^σ (y :^π A) → B
	-}

).

---

¹: this is a direct adaptation from Treloar's rules, see page 13 of their thesis
²: this is actually the same rule as Treloar's, with different naming conventions