Typed Assembly Language (2000)

> I’m an expert and I find it very frustrating

So you say, but I think _I'm_ an expert too, and I wasn't frustrated in the slightest. Maybe you're just not an expert in this space. Did you consider that?

Of course it would be nice if everyone communicated to us in our preferred way, but I think making the reader work a little bit before they have a conversation is a good way to figure out if you're dealing with an expert or not, because an expert actually worth talking to about your ideas will not find it to be too much work to understand them

Students can especially benefit from this advice, because they are still too new to be able to recognise experts from the substance of their words

Thanks for the tip ! I'm very often on the phone for HN and I could not have done it easily. But I promise next time I'll post a big chunk of code I'll do it from my laptop, from where I can easily add 2 spaces at the beginning of each line.

Here is the code edited from my laptop ;)

  open Op;; open Var;; open Ctx;; open Ltal;; open Util;;

  let debug msg = ();;

  let rs = mkvar "rs";; let ra = mkvar "ra";; let rf = mkvar "rf";; let rt = mkvar "rt";; let rr = mkvar "rr";; let ru = mkvar "ru";;

  let retty stackty aty = (Code(Ctx.from_list[(rs,stackty); (ra,aty); (rt,toptp); (rf,listtp); (rr,toptp)]))

  let rec tt tctx ctx tp = match tp with Il.TVar a -> if bound tctx a then TVar a else lookup ctx a | Il.Int -> DTp Word | Il.Top -> DTp Top (* for now ) | Il.Tensor(t1,t2) -> Ref(Tcltal.mkpair (tt tctx ctx t1, tt tctx ctx t2)) | Il.Exists (alpha, tp) -> let beta = rename alpha in Exists (beta, W, tt tctx (extend ctx alpha (TVar beta)) tp) | Il.List t -> let tv = mkvar "list" in Mu(tv,NRef(Tcltal.mkpair(tt tctx ctx t, TVar tv))) | _ -> DTp(arrowtt tctx ctx tp)

  and arrowtt tctx ctx t = match t with Il.Forall(alpha,t) -> let beta = Var.rename alpha in Forall(beta, W, arrowtt tctx (extend ctx alpha (TVar beta)) t) | Il.Arrow(t1,t2) -> let t1' = tt tctx ctx t1 in let t2' = tt tctx ctx t2 in let stk = mkvar "s" in Forall (stk,M, Code(Ctx.from_list[(rs,Stack(Tensor(t1',MTVar stk))); (ra,toptp); (rt,toptp); (rf,listtp); (rr,DTp(retty (Stack(MTVar stk)) t2'))]))

    | _ -> tcfail "expected a function type in forall"

  let typetrans tctx tp = tt tctx Ctx.emp tp let arrowtypetrans tctx t1 t2 = arrowtt tctx Ctx.emp (Il.Arrow (t1,t2))

  ( Need to specify the type ty of "the rest of the stack", in most cases alpha )

  type code_env = {cctx : cctx; cs : code_section; fctx : Il.ctx; lctx : var Ctx.ctx; fp : int}

  let get_fctx cenv = cenv.fctx let get_lctx cenv = cenv.lctx

  type block_env = {cenv : code_env; ilist : instruction list; lab : clab; tctx : Ltal.tctx; rctx : Ltal.rctx}

  let get_from_cenv f benv = f benv.cenv

  exception CodeFail of string code_env exception BlockFail of string * block_env

  (* val begin_fn : code_env -> clab -> register_file -> block_env val end_fn : block_env -> code_env val emit_label : fn_env -> clab -> dtp -> block_env val emit : block_env -> instruction -> block_env -> block_env val emit_end : end_instruction -> block_env -> fn_env val drop : reg -> block_env -> block_env val free : reg -> block_env -> block_env val push : reg -> reg -> block_env -> block_env val pop : reg -> reg -> block_env -> block_env val malloc : reg -> block_env -> block_env )

  let do_print y x = (debug y; x)

  let (>>) f g x = g(f(x)) let (>>=) f h x = let y = f x in h y x

  let rec mkltp tctx rctx = Ctx.fold (fun t sk dtp -> let k = match sk with _,W -> W | _,M -> M in Forall(t,k,dtp)) tctx (Code (rctx))

  let current_ltp benv = debug ("Generalizing "^(Ctx.pp_ctx (fun _ -> "") benv.tctx)^"\n"); ( rt is caller-save *) let rctx = update benv.rctx rt toptp in (mkltp benv.tctx rctx)

So if your algorithm counts apples and counts pears, those wouldn't both have the type "integer". Far from it. They would have the types "number of apples" and "number of pears".

Any 3x3 vec (position 3, velocity 3, rotation 3) that would be more than that, a class specific to an aircraft, would be something much more. It would have position and velocity, and then it would have functions (getters, setters, or prediction functions). Something about the way OP said this was "a type" makes me very suspicious, because those raw values ought to be what you get when you poll the x vx rx ... of the type. If you're getting some sort of interpolation from that, it would obviously need to be from something which extended the type of an object in a certain position and attitude.

The reason I'm saying this is that this is exactly where terrible feedback loops occur, when a type may return an altered version of its basic data when trying to access the basic data.

If it's a type which has an underlying 3x3 vec and this type is specific to the aircraft so it has a bunch of overriding functions to operate on that data, that's fine, that's called a computer program. Not a specific type extending a vector.

    Temperature_C != Temperature_F != int8

I suppose. But you could just as easily do this with C as the target language and then invoke a C compiler. Or just generate machine code directly. It's not clear what assembly specifically provides.

> No need to be a dick.

But there was a need for you to characterise me so?

> So what problem is this solving?

What makes you ask me that instead of reading the website and papers for yourself? Do you think I could possibly know enough about the kinds of other problems you have from the example one that makes you call me names?

I mean, did you read even the first page of the paper I suggested? Were you confused by anything in the first paragraph? Do you know what System-F means in that context? Did you do an Internet search? Anything? Anything at all you could say you got stuck on that you didn't understand? Or did you somehow get the impression I should spoon-feed you?

Why do you waste anyones time with this?