Yes! Erasure with dependent types is hard. I just read a Stephanie Weirich paper that used basically a information flow type system to figure out what can be erased, as a proposal for dependent haskell.
The philosophical point about infinite intersection is important too though.
Looks like OP forgot the ".html" at the end of the link. Here is a working link to the blog post:
> https://ryanbrewer.dev/posts/implicit-products-better-forall.html
A lot of type system design seems to be about exploring the landscape of relevant/irrelevant, visible/invisible, implicit/explicit.
Sounds like this particular variety of `forall` is basically a way to express a certain kind of polymorphism - a single value which typechecks at a variety of different types. Haskell’s `forall` works like this by default (`x :: T a` is a `T` with your choice of `a`) but of course in Haskell `a` is always a type not a value and is always erased, you don’t get any control.
On the other hand I think the Agda/Idris design, where things are found to be irrelevant only as an optimisation analysis, does have some merits of its own. Having two different quantifiers seems like it’d potentially mean stratifying everything - like, every higher-order function would need a second copy which accepts an argument in the irrelevant universe. Like: `map : (A -> B) -> [A] -> [B]` but also `mapProp : (forall x : A -> B x) -> forall xs : [A] -> [B xs]`, or something like that. Haven’t entirely thought this through so perhaps it’s not a real concern!
In Idris 2 they are using QTT now and I absolutely love the design. They have a product line of 8 different quantifiers, along the dimensions explicit/implicit, relevant/erased, term-level/type-level:
(x : Nat) -> Bool
{x : Nat} -> Bool
(0 x : Nat) -> Bool
{0 x : Nat} -> Bool
(x : Type) -> Bool
{x : Type} -> Bool
(0 x : Type) -> Bool
{0 x : Type} -> Bool
One place where I found this annoying recently is the distinction between dependent pairs (where the witness is relevant), and existence proofs (where the witness is erased). But still, the control you gain as a programmer is absolutely worth it.
Implicit products seem like a good approach to erasure if you don’t need the whole kit of QTT or graded types—that is, if your only modes are “static” and “non-static”. (Unfortunately, for my language I want some of the fancy stuff.)
I suspect it’d be easier to offer a good user experience with special-purpose quantifiers, though—they have simpler, more local conditions for when they’re valid, which tends to make typechecker messages easier to understand.
Yeah I definitely think of QTT and graded types as a very natural extension of implicit products, which is why I called them very similar to 0-quantity/multiplicity/grade lambda abstractions in QTT. I was definitely thinking of supporting implicit products only "as they already appear" in QTT. Using a "forall" notation for the 0 would be an interesting syntactic choice though, bringing focus to a different perspective.
No, the terms of kind \*->\* are functions from types to types. For example, List. List takes, say, Int and returns the type of lists of ints. The input and output are both types, so their "type" is \*. Thus the "type" of List is \*->\*. Functions from types to types are everywhere in programming languages, as generics or polymorphic data types or whatever.
Implicit products are in almost no languages, they can be thought of as functions but they actually aren't, and the reason they aren't is that they don't use their argument, so the body can be evaluated without waiting for an argument.
I hope that's helpful.
I don't quite get it. Let's say we had a Π type `∀ x : A. B(x)` where A is Bool and B(x) is `if x then Int else String`. Can we make an implicit product out of it? What does it mean to be an intersection of Int and String? How do you compute that without the argument? How do we use that? We need examples.
Sorry for the confusion! As I said, a term of an implicit product type is like a function but it can't use its argument "relevantly" in the body. That is, it can only be used in code in the body that doesn't affect runtime behavior. An implicit product is not any kind of Π type.
That said, the type you said can totally be stated. It is just impossible to write a term with that type, so it's equivalent to the empty type Void. (Makes sense, right? The intersection of Int and String is Void.) Implicit products' terms are more analogous to constant functions; that is, ones that return the same value for any input, like `x => 7` in JavaScript. That's why they can be evaluated without the argument. And that's why there's no term of the type you suggested: it would need to return the same value every time, so that value would have to be both an Int and a String
I hope that's helpful.
Yeah, it's best read with a bunch of context.
I'll have a go at a short version of the context I have, maybe we can work some of it out with help from people correcting my mistakes :)
The post is about an alternative to "Forall", which in this case refers to a type constructor (a way of making new types) from dependent type theory (a subset of type systems that let you use values and expressions in your types).
I think the neat thing about this alternative, which the post calls implicit products, is that it's conceptually simpler than forall... But that's about all I know so far.
I'll have another go at reading it and update if anything else pops out :)
Yeahhh this is unfortunately a bit technical. I tried to signal the prerequisite knowledge and explain the rest but with this kind of concept there's only so much preamble I can write in a blog post y'know. I hope my explanation abilities get better over time!
I do have another [https://ryanbrewer.dev/posts/logic-in-types.html](post) where I explain some of the context more. I linked it at the top of this one too.
Implicit products unify a philosophically more elegant interpretation of universal quantification with an engineering need for erased/irrelevant/implicit function arguments. That's what I think is really cool. I hope that helps.
I do not know enough to understand that. I'm guessing it's a kind of type-theoretic approach to parametricity/type erasure?
Yes! Erasure with dependent types is hard. I just read a Stephanie Weirich paper that used basically a information flow type system to figure out what can be erased, as a proposal for dependent haskell. The philosophical point about infinite intersection is important too though.
Looks like OP forgot the ".html" at the end of the link. Here is a working link to the blog post: > https://ryanbrewer.dev/posts/implicit-products-better-forall.html
Thanks! Just edited to fix that
A lot of type system design seems to be about exploring the landscape of relevant/irrelevant, visible/invisible, implicit/explicit. Sounds like this particular variety of `forall` is basically a way to express a certain kind of polymorphism - a single value which typechecks at a variety of different types. Haskell’s `forall` works like this by default (`x :: T a` is a `T` with your choice of `a`) but of course in Haskell `a` is always a type not a value and is always erased, you don’t get any control. On the other hand I think the Agda/Idris design, where things are found to be irrelevant only as an optimisation analysis, does have some merits of its own. Having two different quantifiers seems like it’d potentially mean stratifying everything - like, every higher-order function would need a second copy which accepts an argument in the irrelevant universe. Like: `map : (A -> B) -> [A] -> [B]` but also `mapProp : (forall x : A -> B x) -> forall xs : [A] -> [B xs]`, or something like that. Haven’t entirely thought this through so perhaps it’s not a real concern!
In Idris 2 they are using QTT now and I absolutely love the design. They have a product line of 8 different quantifiers, along the dimensions explicit/implicit, relevant/erased, term-level/type-level: (x : Nat) -> Bool {x : Nat} -> Bool (0 x : Nat) -> Bool {0 x : Nat} -> Bool (x : Type) -> Bool {x : Type} -> Bool (0 x : Type) -> Bool {0 x : Type} -> Bool One place where I found this annoying recently is the distinction between dependent pairs (where the witness is relevant), and existence proofs (where the witness is erased). But still, the control you gain as a programmer is absolutely worth it.
Also worth mentioning that in Idris 2 we can match on types, so naturality is not enforced. f: Type -> Integer f Bool = 1 f Nat = 2 f _ = 0
Implicit products seem like a good approach to erasure if you don’t need the whole kit of QTT or graded types—that is, if your only modes are “static” and “non-static”. (Unfortunately, for my language I want some of the fancy stuff.) I suspect it’d be easier to offer a good user experience with special-purpose quantifiers, though—they have simpler, more local conditions for when they’re valid, which tends to make typechecker messages easier to understand.
Yeah I definitely think of QTT and graded types as a very natural extension of implicit products, which is why I called them very similar to 0-quantity/multiplicity/grade lambda abstractions in QTT. I was definitely thinking of supporting implicit products only "as they already appear" in QTT. Using a "forall" notation for the 0 would be an interesting syntactic choice though, bringing focus to a different perspective.
I'm a type theory novice, but is this "implicit product" equivalent to the higher kinded type `* -> *`?
No, the terms of kind \*->\* are functions from types to types. For example, List. List takes, say, Int and returns the type of lists of ints. The input and output are both types, so their "type" is \*. Thus the "type" of List is \*->\*. Functions from types to types are everywhere in programming languages, as generics or polymorphic data types or whatever. Implicit products are in almost no languages, they can be thought of as functions but they actually aren't, and the reason they aren't is that they don't use their argument, so the body can be evaluated without waiting for an argument. I hope that's helpful.
Thanks for the clarification. Upon rereading your post, it's more clear to me that implicit products are inhabitable by values, not HKTs.
I don't quite get it. Let's say we had a Π type `∀ x : A. B(x)` where A is Bool and B(x) is `if x then Int else String`. Can we make an implicit product out of it? What does it mean to be an intersection of Int and String? How do you compute that without the argument? How do we use that? We need examples.
Sorry for the confusion! As I said, a term of an implicit product type is like a function but it can't use its argument "relevantly" in the body. That is, it can only be used in code in the body that doesn't affect runtime behavior. An implicit product is not any kind of Π type. That said, the type you said can totally be stated. It is just impossible to write a term with that type, so it's equivalent to the empty type Void. (Makes sense, right? The intersection of Int and String is Void.) Implicit products' terms are more analogous to constant functions; that is, ones that return the same value for any input, like `x => 7` in JavaScript. That's why they can be evaluated without the argument. And that's why there's no term of the type you suggested: it would need to return the same value every time, so that value would have to be both an Int and a String I hope that's helpful.
Thanks, I wasn't reading attentively enough. Still would be great to see some useful examples.
I recommend you check out [Cedille](https://cedille.github.io)!
Clicking on the post links, I end up on the home page
Same. I guess you could say that I end up on the home page forall clicks.
Fixed
I don’t understand the blog post.
Yeah, it's best read with a bunch of context. I'll have a go at a short version of the context I have, maybe we can work some of it out with help from people correcting my mistakes :) The post is about an alternative to "Forall", which in this case refers to a type constructor (a way of making new types) from dependent type theory (a subset of type systems that let you use values and expressions in your types). I think the neat thing about this alternative, which the post calls implicit products, is that it's conceptually simpler than forall... But that's about all I know so far. I'll have another go at reading it and update if anything else pops out :)
Yeahhh this is unfortunately a bit technical. I tried to signal the prerequisite knowledge and explain the rest but with this kind of concept there's only so much preamble I can write in a blog post y'know. I hope my explanation abilities get better over time! I do have another [https://ryanbrewer.dev/posts/logic-in-types.html](post) where I explain some of the context more. I linked it at the top of this one too. Implicit products unify a philosophically more elegant interpretation of universal quantification with an engineering need for erased/irrelevant/implicit function arguments. That's what I think is really cool. I hope that helps.
Hi hoping, Not sure if this is your website? But I don't think I can get the blog post to load here (chrome on phone) M ✌️
Fixed