andrew-johnson-4/LSTS

Isolate type rules for conjunction types

andrew-johnson-4 opened this issue · 2 comments

andrew-johnson-4 commented

Is your feature request related to a problem? Please describe.
It would be nice to share a minimal implementation of conjunction types that could be applied to a generic functional language.

  • Introduction
  • Inference
  • Subtyping
  • Projection
andrew-johnson-4 commented

Make introduction explicit for consistency with Rust style trait system.

Introduction

$$\frac{\Gamma,x:A,x:B \ \ x:A+B}{\Gamma,x:A+B}$$