Idea for inferring and constraining structural types...

static_type_inference.txt

// `@foo` is a symbol that can be treated as a type or a value

// `a :: T` is a forward type declaration where value `a` is of type `T`
// I'm using this for mainly for explanatory purposes to show what structural
// type inference might allow for

// `<'x>` declares a type variable `'x`
// I've prefixed the type variables with an apostrophe to make clear what is a
// regular type and what a type variable is (borrowing from F#/OCaml notation)
//
str <'x> :: ({ name: string }) -> string
fn str(x) {
  x.name
}

let user = { name: "jaxrtech" }
str(user)
//
// > val :: string
// > "jaxrtech"

// Probably could just use the dot operator for pushing the value on the lhs
// to the first argument going back to the unified functional call proposal
//

user.str()
//
//> val :: string
//> val = "jaxrtech"


apply_damage <'entity, 'attack> ::
  ( 'entity: { hp: int }
  , 'attack: { damage: int } )
  -> 'entity

fn apply_damage(entity, attack) {
  entity.hp -= attack.damage
}


let player =
  { tag = @player
  ; name = "The Hero"
  ; hp = 500
  ; position = (10, 32)
  }

let sword =
  { tag = @weapon
  ; damage = 65
  }

let bandit =
  { tag = @enemy
  ; name = "Random Bandit"
  ; hp = 100
  ; damage = 50 
  }

apply_damage(player, bandit)
//
//> val :: player (actual type of variable `player`)
//> val :: { tag: @player; name: string, hp: int, position: (int, int) }
//
//> val = { tag: @player; name: "The Hero", hp: 450, position: (10, 32) }


// ~~~

// Now for a more extreme example using a really basic expression interpreter
//

// In other words, you should be able to just type this and get static typing
// for free

fn eval(x) {
  match x.tag {
    @num =>
      x.value
    
    @binary_op =>
      let f = match (x.op) {
        @add => (+)
        @sub => (-)
        @mul => (*)
        @div => (/)
      }

      f(x.lhs, x.rhs)
  }
}

// 42
eval({ tag = @num; value = 42 })
//
// val :: int
// val = 42

// To make life a bit easier with some functions (you probably could even just
// make this work implicitly or something nicer)
num <'x> :: ('x) -> { tag: @num; value = 'x }
fn num(x) {
  { tag: @num; value = x }
}

// 1 + 2
eval({ tag = @binary_op; lhs = num(1); rhs = num(2) }) 
//
// val :: int
// val = 3


// (3 * 5) + 2
expr ::
  { tag = @binary_op
  ; lhs =
      { tag = @binary_op
      ; lhs = { tag: @num; value = int }
      ; rhs = { tag: @num; value = int }
      }
    rhs =
      { tag: @num; value = int }
  }

let expr =
  { tag = @binary_op
  ; lhs =
      { tag = @binary_op
      ; lhs = num(3)
      ; rhs = num(5)
      }
    rhs =
      num(2)
  }

eval(expr) 
//
// val :: int
// val = 3


// ... going back to the originally defined `eval()` function which was:

fn eval(x) {
  match x.tag {
    @num =>
      x.value
    
    @binary_op =>
      let f = match (x.op) {
        @add => (+)
        @sub => (-)
        @mul => (*)
        @div => (/)
      }

      f(x.lhs, x.rhs)
  }
}

// the `eval()` functional really would look something like the following mess
// in terms explicit type declarations that the type inference should otherwise
// give you for free
//
// I had to name the otherwise anonymous types because it kind tedious for
// explanatory purposes

eval <'a, 'x> ::             
  ( 'a =
      ENum =
        { tag: @num
        ; value: 'x
        }

    | EBinaryOp =
        <'l, 'r>            // type variables in current scope
        { tag: @binary_op
        ; op: @add | @sub | @mul | @div
        ; lhs: 'l when eval('l) -> 'x // constraint where type variable `'l` has 
        ; rhs: 'r when eval('r) -> 'x // to be the same type of the parameter in
        ;                             // `eval`
        }
  )
  -> 'x
    when
    ( ('a : ENum)
    | ('a : EBinaryOp)
        & ( ((x.op : @add) & ('l + 'r : 'x))
          | ((x.op : @sub) & ('l - 'r : 'x))
          | ((x.op : @mul) & ('l * 'r : 'x))
          | ((x.op : @div) & ('l / 'r :  x))
          )
    )

fn eval(x) {
  x.tag :: @num | @binary_op

  match x.tag {
    @num =>
      a :: $eval
      let a = x.value
      
      a
    
    @binary_op =>
      x.op :: @add | @sub | @mul | @div

      f <'a, 'b, 'c> ::    // type variables that will be constrained
          ('a, 'b) -> 'c   // the actual signature

          when             // type constraints are prefixed by `when`
            
            // requires that `x.op` was type `@add`
            ((x.op : @add)

            // *and* that you can `(+)` type variable `'a` and type variable `'b`
            // which must evaluate to type variable `c`
             & ('a + 'b : 'c))

          | ((x.op : @sub) & ('a - 'b : 'c))  // the rest of the type constraints
          | ((x.op : @mul) & ('a * 'b : 'c))  // (extra parentheses to be explicit)
          | ((x.op : @div) & ('a / 'b : 'c))

      let f = match (x.op) {
        // you could use `(+)` or something similar 
        @add => (a, b) -> a + b
        @sub => (a, b) -> a - b
        @mul => (a, b) -> a * b
        @div => (a, b) -> a / b
      }

      x.lhs :: eval($a)
      let lhs = eval(x.lhs)

      x.rhs :: eval($a)
      let rhs = eval(x.rhs)

      result :: $f
      let result = f(lhs, rhs)

      result
  }
}