Conversation

Rob Rix‎
@rob_rix
(obvs if the lang/field is strict, that doesn’t work.) so the records you’re thinking of are strict ones. in a polarized lang, that’s probably the same as positive records.
2
Rob Rix‎
@rob_rix
functions are negative, and on the theory side you can see the distinction in the intro rule (showing just the types for the moment): Γ, A ⊢ B ----- Γ ⊢ A -> B here, proving the premise doesn’t actually require an A—all that we need to do is to hypothesize that A exists
1
1
Rob Rix‎
@rob_rix
extending the context with a variable (here, a proposition) is the same thing as hypothesizing or assuming. we are saying “if we can get there under the assumption of A, then we can definitely get there if you actually give us an A”
1
Rob Rix‎
@rob_rix
by contrast, the judgement for a (strict) pair (written ⊗) works a little differently; we’ll look at the elim rule (for reasons that are unlikely to be obvious), with proof terms: Γ ⊢ x : Y ⊗ Z Γ, y : Y, z : Z ⊢ b : C ---- Γ ⊢ case x of (y, z) -> b : C
1
Rob Rix‎
@rob_rix
here again we have assumptions, but since they’re present for elimination, that means they’re eager—this is a redex, so we have to have the values of y and z ready to do anything with it. by contrast, good ol’ ✕ is eliminated by a pair of projections, neither of which extends Γ
1
Rob Rix‎
@rob_rix
the other part of this distinction is that a datatype constructor is not a function. Haskell (among others) conveniently introduces functions with the same name as the constructor so that you can write Foo x y where Foo is ternary and get a function Z -> Foo, but…
1
Rob Rix‎
@rob_rix
…the actual datatype constructor has to be fully saturated or not at all. (in Facet I do this by just synthesizing constructor _functions_ when I elaborate the datatype declaration.)
1
Rob Rix‎
@rob_rix
so that can make the space a little weirder if you have both record-style construction syntax and function-style construction syntax for records, like Haskell does, i.e. Foo { a = x, b = y, c = z } and Foo x y z
1
1