Conversation

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

Brendan Zabarauskas

@brendanzab

Apr 3, 2021

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!

Rob Rix‎

@rob_rix

Apr 3, 2021

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 :\

Replying to

and

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.

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

Replying to

and

it’s a pretty important—and thus far rather underserved—area of study IMO!

Brendan Zabarauskas

@brendanzab

Apr 3, 2021

Been pretty excited with

@jonmsterling

and Harper's draft paper which addresses some of my terrors to do with trying to move around in this space (I think it'll still involve a lot of me bumbling around in the dark, but it's a big help)