[Questions] Various questions on the article

[Heimdell]

I've just read the paper.

Not that I understand it fully, but I think the separation onto t- and t+ is promising. It looks like it solves subtyping (which is inevitable in case of rank-N polymorphism).

There are my questions: 1) The subi(mu a. t1+, mu b. t2-) can loop, because the record can be both positive and negative, so subi(mu a. {f: a} =< mu b. {f: b}) => subi({f: mu a. {f: a}} =< {f: mu b. {f: b}}) => subi(mu a. {f: a} =< mu b. {f: b}), which is a loop, so we need a rule that biunifies two mu-types in assumption that a =< b.

2) The conversion to automata and back is slightly unclear; can you elaborate on it? I'd implement it by grouping constraints into functions, records and so on and then using distributivity in reverse, instead of, ya know, all that automata stuff.

3) Is it possible to shove in rank-N types? Probably, in form of id: /\ {A: *}. \a: A -> a, where {}-params are inferred.

4) ~Is it possible to infer the type of function to be (bool \/ (A -> B)) -> Res, which is usable? Doesn't it mean, that it is also possible to infer type Res -> (bool /\ (A -> B)), which for practical purposes is Res -> Bottom and unusable?~ Nevermind, I just mixed t+ and t- here.

5) Is it possible to add type classes into the mix - probably as records in negative form?

[jfaure]

Hi, Thanks for the interest ! To answer your questions:

1. Type Polarity is a bit abstract, it depends on the position we're considering the type from. The inference algorithm conveniently only generates polar types types (at no loss of generality), but this is not a theoretical restriction on the types. Here is how subi decomposes records (pg 83): subi({1 : t+1 . . . n : t+n. . . (n+k) : t+(n+k) } <? {1 : t−1 . . . n : t−n}) = {t+1 <? t−1 . . . t+n <? t−n} we see that when considering a record in a given polarity, we consider it's fields with the same polarity. A different polarity type may arise if we consider a contravariant structure (eg. the function type d- -> r+), and indeed those require recursive binders.

2. I am also not a fan of the Automata, the conversion boils down to considering type variables as pointers rather than indexes into a table, so while the concept is helpful to deepen ones understanding, I do not use it.

Side-note: Biunification does not create then solve a constraint set, rather it biunifies constraints on the fly as they arise... which I believe is one of the most genius innovations since it gives us enormous flexibility on how to identify and handle constraints.

3. Rank-N types are available, I even believe it is possible to infer them (aka. impredicative polymorphism) using the ideas from Rémy's ML^F - The subtyping theory tells us that type variables are only affected by occurences of types in the same polarity - with the key exception being higher rank types. My idea is to use the unification of MLF to relate the two, which is attractive since it doesn't interfere with the subtyping inference except to create new type variables when higher-rank types are in play. (Recall the key takeaway from ML^F is that inference is decidable in the presence of judiciously placed 'oracles'). Satisfyingly, biunification also gives us the same utility as the bidirectional inference mechanisms used in Agda for implicit arguments. I'm working on inductive families, but this is next.

4. Happened to me often enough.

5. Typeclasses are available thanks to record subtyping, implicit arguments and inference, but in a different form. I would mention also that the formulation of a haskell style typeclass is a theoretical anomaly, with it's prolog-like unification, non-extensionability, orphan-instances, coherence-issues and lack of subtyping; problems which arise from the unnatural leap of packing a typeclass language atop Haskell.

James

---

From: Андреев Кирилл notifications@github.com Sent: Wednesday, July 29, 2020 10:59 PM To: jfaure/Nimzo Nimzo@noreply.github.com Cc: Subscribed subscribed@noreply.github.com Subject: [jfaure/Nimzo] [Questions] Various questions on the article (#2)

I've just read the paper.

Not that I understand it fully, but I think the separation onto t- and t+ is promising. It looks like it solves subtyping (which is inevitable in case of rank-N polymorphism).

There are my questions:

1. The subi(mu a. t1+, mu b. t2-) can loop, because the record can be both positive and negative, so subi(mu a. {f: a} =< mu b. {f: b}) => subi({f: mu a. {f: a}} =< {f: mu b. {f: b}}) => subi(mu a. {f: a} =< mu b. {f: b}), which is a loop, so we need a rule that biunifies two mu-types in assumption that a =< b.

2. The conversion to automata and back is slightly unclear; can you elaborate on it? I'd implement it by grouping constraints into functions, records and so on and then using distributivity in reverse, instead of, ya know, all that automata stuff.

3. Is it possible to shove in rank-N types? Probably, in form of id: /\ {A: *}. \a: A -> a, where {}-params are inferred.

4. Is it possible to infer the type of function to be (bool \/ (A -> B)) -> Res, which is usable? Doesn't it mean, that it is also possible to infer type Res -> (bool /\ (A -> B)), which for practical purposes is Res -> Bottom and unusable? Nevermind, I just mixed t+ and t- here.

5. Is it possible to add type classes into the mix - probably as records in negative form?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/jfaure/Nimzo/issues/2, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AGRCMEF4V5MO3EAOJP4EZ73R6CES5ANCNFSM4PMAZQWA.

[jfaure]

I misunderstood the first question slightly, indeed there is a rule for decomposing a recursive binder: subi(t+ <= µα.t− ) = {t+ <= t− [µα.t − /α]}

---

From: james faure james.faure@epitech.eu Sent: Thursday, July 30, 2020 7:19 AM To: jfaure/Nimzo reply@reply.github.com Subject: Re: [jfaure/Nimzo] [Questions] Various questions on the article (#2)

Hi, Thanks for the interest ! To answer your questions:

1. Type Polarity is a bit abstract, it depends on the position we're considering the type from. The inference algorithm conveniently only generates polar types types (at no loss of generality), but this is not a theoretical restriction on the types. Here is how subi decomposes records (pg 83): subi({1 : t+1 . . . n : t+n. . . (n+k) : t+(n+k) } <? {1 : t−1 . . . n : t−n}) = {t+1 <? t−1 . . . t+n <? t−n} we see that when considering a record in a given polarity, we consider it's fields with the same polarity. A different polarity type may arise if we consider a contravariant structure (eg. the function type d- -> r+), and indeed those require recursive binders.

2. I am also not a fan of the Automata, the conversion boils down to considering type variables as pointers rather than indexes into a table, so while the concept is helpful to deepen ones understanding, I do not use it.

Side-note: Biunification does not create then solve a constraint set, rather it biunifies constraints on the fly as they arise... which I believe is one of the most genius innovations since it gives us enormous flexibility on how to identify and handle constraints.

3. Rank-N types are available, I even believe it is possible to infer them (aka. impredicative polymorphism) using the ideas from Rémy's ML^F - The subtyping theory tells us that type variables are only affected by occurences of types in the same polarity - with the key exception being higher rank types. My idea is to use the unification of MLF to relate the two, which is attractive since it doesn't interfere with the subtyping inference except to create new type variables when higher-rank types are in play. (Recall the key takeaway from ML^F is that inference is decidable in the presence of judiciously placed 'oracles'). Satisfyingly, biunification also gives us the same utility as the bidirectional inference mechanisms used in Agda for implicit arguments. I'm working on inductive families, but this is next.

4. Happened to me often enough.

5. Typeclasses are available thanks to record subtyping, implicit arguments and inference, but in a different form. I would mention also that the formulation of a haskell style typeclass is a theoretical anomaly, with it's prolog-like unification, non-extensionability, orphan-instances, coherence-issues and lack of subtyping; problems which arise from the unnatural leap of packing a typeclass language atop Haskell.

James

---

From: Андреев Кирилл notifications@github.com Sent: Wednesday, July 29, 2020 10:59 PM To: jfaure/Nimzo Nimzo@noreply.github.com Cc: Subscribed subscribed@noreply.github.com Subject: [jfaure/Nimzo] [Questions] Various questions on the article (#2)

I've just read the paper.

Not that I understand it fully, but I think the separation onto t- and t+ is promising. It looks like it solves subtyping (which is inevitable in case of rank-N polymorphism).

There are my questions:

1. The subi(mu a. t1+, mu b. t2-) can loop, because the record can be both positive and negative, so subi(mu a. {f: a} =< mu b. {f: b}) => subi({f: mu a. {f: a}} =< {f: mu b. {f: b}}) => subi(mu a. {f: a} =< mu b. {f: b}), which is a loop, so we need a rule that biunifies two mu-types in assumption that a =< b.

2. The conversion to automata and back is slightly unclear; can you elaborate on it? I'd implement it by grouping constraints into functions, records and so on and then using distributivity in reverse, instead of, ya know, all that automata stuff.

3. Is it possible to shove in rank-N types? Probably, in form of id: /\ {A: *}. \a: A -> a, where {}-params are inferred.

4. Is it possible to infer the type of function to be (bool \/ (A -> B)) -> Res, which is usable? Doesn't it mean, that it is also possible to infer type Res -> (bool /\ (A -> B)), which for practical purposes is Res -> Bottom and unusable? Nevermind, I just mixed t+ and t- here.

5. Is it possible to add type classes into the mix - probably as records in negative form?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/jfaure/Nimzo/issues/2, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AGRCMEF4V5MO3EAOJP4EZ73R6CES5ANCNFSM4PMAZQWA.

[Heimdell]

Thanks for the answers.

1. What if we work on subi(µα.t+ <= µb.u-) and t+ and u- have their recursion point at the same place?

[jfaure]

I'm not sure I understand the question, we need to ensure uniqueness of fixed-points for correctness. Mutual recursion presents no difficulties, partly due to the guardedness requirement (occurrences of α inside µα.t must be underneath at least one → or { . . . }) If you're thinking of iso-recursive data-types (as opposed to the equirecursive ones considered for typing functions), those can be added easily with opaque roll/unroll operations at constructor application.

The point of the µ binder is to avoid infinitely unrolling function types: `(µα.bool → α) → ⊥ →

(bool → ⊥) → ⊥

→

((bool → bool → ⊥) → ⊥`

[Heimdell]

No, I just think that mutually recuring into two fixpoints if their structure is the same will cause loop and make typechecker hang, because we will meet mu t <= mu t again. So, the first question is - can the - and + mu-types have the same structure at any point?

[jfaure]

Ah right, that is handled using a memoisation table for type variables, see section 5.4.7 I'm not sure if it would be sufficient to only consider the case where two recursive types meet directly...