What System-F• could look like?

doodle.txt

type Maybe: * -> *
Just: forall t: *. t -> Maybe t
Nothing: forall t: *. Maybe t

type Array: * -> 1 -> *
type Array t a = {
  length: a -> (Int, a),
  get: (Int, a) -> (t, a),
  set: (Int, t, a) -> a,
}

makeArray: forall t: *. (Int, t) -> exists a: 1. (a, Array t a)
makeArray[t](len, initVal) =
  let ptr = unsafeMalloc(length * sizeof(t))
  in pack a = (UnsafePtr, Int) in ((ptr, len), {
    length(_, len) = len,
    get(index, (ptr, len)) = unsafePtrGet[t](ptr, len * sizeof[t]),
    set(index, value, (ptr, len)) = unsafePtrSet[t](ptr, len * sizeof[t], value),
  })

type Dict: * -> * -> 1 -> *
type Dict k v d = {
  get: (k, d) -> (v, d),
  set: (k, v, d) -> d,
}

makeDict: forall k: *, v: *. () -> exists d: 1. (d, Dict k v d)
makeDict[k,v]() =
  let
    keyArray = makeArray[k](0, undefined[k])
    valueArray = makeArray[v](0, undefined[v])
  in pack d = (Array k a, Array v b) in ((keyArray, valueArray), {
    get(key, (keyArray, valueArray)) =
      let
        checkIndex: forall a: 1, b: 1. (Int, Array k a, Array v b) -> (Maybe v, Array k a, Array v b)
        checkIndex[a, b](index, keyArray, valueArray) =
          if index < keyArray.length()
          then
            if keyArray.get(index) == key
            then (Just(valueArray.get(index)), keyArray, valueArray)
            else checkIndex(index + 1, keyArray, valueArray)
          else (Nothing, keyArray, valueArray)
      in checkIndex(0, keyArray, valueArray)
    set(key, value, (keyArray, valueArray)) =
      let
        checkIndex: forall a: 1, b: 1. (Int, Array k a, Array v b) -> (Array k a, Array v b)
        checkIndex[a, b](index, keyArray, valueArray) =
          if index < keyArray.length()
          then
            if keyArray.get(index) == key
            then (keyArray, valueArray.set(index, value))
            else checkIndex(index + 1, keyArray, valueArray)
          else let
            let
              newKeyArray = makeArray(keyArray.length() * 2 + 1, undefined[k])
              newValueArray = makeArray(valueArray.length() * 2 + 1, undefined[v])
            in
              moveArray(newKeyArray, 0, keyArray, 0, keyArray.length());
              moveArray(newValueArray, 0, valueArray, 0, valueArray.length();
              (keyArray.set(index, key), valueArray.set(index, value))
      in checkIndex(0, keyArray, valueArray)
  })