aradarbel10

{-# LANGUAGE StrictData, DerivingVia, OverloadedRecordDot #-}

{-
  (compiled with GHC 9.4.2)
-}

{-
  HEADS UP
  this is an example implementation of a non-trivial type system using bidirectional type checking.
  it is...

takahisa

type 'a expr = ..
type 'a expr +=
  | Int: int -> int expr
  | Add: int expr * int expr -> int expr
  | Sub: int expr * int expr -> int expr

effect Extension: 'a expr -> 'a

let rec eval1: type a. a expr -> a = function
  | Int n0 -> n0