Conversation

ok so! this is sort of an evaluation order thing. in a lazy lang you can construct a record w/o providing each field by using e.g. fix id as the value of the field—something divergent—and just not touching it

Rob Rix‎

@rob_rix

Apr 3, 2021

(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.

Rob Rix‎

@rob_rix

Apr 3, 2021

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

Rob Rix‎

@rob_rix

Apr 3, 2021

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”

Rob Rix‎

@rob_rix

Apr 3, 2021

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

Rob Rix‎

@rob_rix

Apr 3, 2021

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 Γ

Rob Rix‎

@rob_rix

Apr 3, 2021

(cf existentialtype.wordpress.com/2012/08/25/pol for more details. I actually find the argument about polarity in relation to products a tiny bit weak since you could presumably push thunks into the context, but that would certainly not be minimal.)

Rob Rix‎

@rob_rix

Apr 3, 2021

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…

Rob Rix‎

@rob_rix

Apr 3, 2021

…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.)

Rob Rix‎

@rob_rix

Apr 3, 2021

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

Replying to

and

Tbh I'm thinkin of going the other way - having a record-like syntax for functions - where functions always have named args. It might be a bit weird though!

6:23 AM · Apr 3, 2021Twitter Web App

Replying to

and

Like, I'm building in records to my core language - ie. labelled sigma types, and it feels a bit weird not to also have labelled product types… but maybe *I'm* the weird one.

Rob Rix‎

@rob_rix

Apr 3, 2021

eh this is all the edge of the bubble, everything’s weird here, go to it and good luck!

Replying to

and

keyword args have a lot to recommend them tho yeah I recall us chatting about some of the challenges in a DT setting. tbh I feel like the ergonomic issues with DTs undermine their utility for non-proof-assistant stuff :\

Brendan Zabarauskas

@brendanzab

Apr 3, 2021

Yeah that's kind of why I want to focus on using them for non-proof-assistant stuff. As an expressive programming system for working with types, terms, and modules in a unified language. but yeah there are indeed annoyances.

Show replies