George ZNov 28

Can I get some help with the Amber rules (Amadio & Cardelli '93) for #subtyping?

I haven't seen mentions that it's possible to derive `μx.x <: t <: μx.x` *for every `t`*.

Here's my proof of the 1st (the 2nd is the same):

```
μx.x <: t ⊢ μx.x <: t
--------------------------
μx.x <: t ⊢ x [μx.x/x] <: t
------------------------------
⬝ ⊢ μx.x <: t
```

What's wrong?

The Amber rules do induction afaik, is the problem that `x` is not under a `+` or `→`?

#type #typesystem #subtype

Hacker NewsMar 29, 2025

You Need Subtyping

https://blog.polybdenum.com/2025/03/26/why-you-need-subtyping.html

#HackerNews #You #Need #Subtyping #subtyping #programming #languages #software #development #tech #insights

Why You Need Subtyping

Ever since Stephen Dolan’s 2016 thesis Algebraic Subtyping showed how to combine type inference and subtyping, I’ve been developing increasingly sophisticated programming languages based on those ideas, first IntercalScript in 2019, then CubiML in 2020, PolySubML in 2025, and with my next language already in the planning stages.

Considerations on Codecrafting
Giuseppe MichieliMay 31, 2024

#Guidance to Commercial #Laboratories on Increasing #Submission of #Influenza A and B Positive Samples to State and Local Public Health Laboratories for Additional #Subtyping (including #H5), #US #CDC: https://www.cdc.gov/flu/avianflu/guidance-commercial-laboratories.htm

Commercial laboratories are encouraged to communicate with the PHL of the patient’s state of residence prior to submitting specimens to obtain the appropriate specimen submission form and any additional submission instructions.

Guidance to Commercial Laboratories on Influenza Specimen Submission

CDC requests commercial laboratories continue to send influenza specimens to PHLs

Centers for Disease Control and Prevention
nopeAug 29, 2023
An Extension of System F with Subtyping
(1994) : Cardelli, L. et al
DOI: https://doi.org/10.1006/inco.1994.1013
#subtyping #system_F #type_inference #my_bibtex
mudgeNov 11, 2022
While I’m being nostalgic, it has been five years since I wrote a lot of words and several ASCII diagrams inspired by @jcoglan in an attempt to understand #TypesAndProgrammingLanguages’ chapter on #Subtyping: https://github.com/computationclub/computationclub.github.io/wiki/Types-and-Programming-Languages-Chapter-15-Subtyping-%E2%80%93-Part-1
Computer Music Workshop · computationclub/computationclub.github.io Wiki

The website of the London Computation Club. Contribute to computationclub/computationclub.github.io development by creating an account on GitHub.

GitHub
nopeJul 30, 2022
A Bidirectional Refinement Type System for Lf
(2008) : William Lovas and Frank Pfenning
DOI: https://doi.org/10.1016/j.entcs.2007.09.021
#LF #dependent_types #intersection_types #refinement_types #subtyping
#my_bibtex
xameerJan 29, 2021
Sqrt - if a #subtype can be defined for the reals, to separate positive and negative reals, two functions can be written for the reals, one to return a real when parameter is + another to return a complex value when it is
Strongly typed
Case for #subtyping #overloading