search

fmease / lushui

The reference compiler of the Lushui programming language
Apache License 2.0
7 stars 0 forks source link

Shared record fields #88

Open fmease opened 3 years ago

fmease commented 3 years ago

Support for compact product-sum-product GADTs. Example:

data Expr: Type of
    ::location: Location
    lit: Nat -> Expr
    add: Expr -> Expr -> Expr

a: Expr = Expr.lit loc0 23
b: Expr = Expr.add (merge loc0 loc1) a (Expr.lit loc1 100)
loc0_: Location = a::location ;;; no case analysis required
m: Unit = case a of
    Expr.lit \_loc val => unit
    Expr.add \_loc left right => unit
fmease commented 2 years ago

This proposal has to be updated to the reflect syntactic changes to records proposed in #109.