[{"_1":2,"_166":-5,"_167":-5},"loaderData",{"_3":4,"_13":14,"_21":22,"_141":142},"root",{"_5":-5,"_6":-7,"_7":8,"_9":-7,"_10":11,"_12":-7},"currentUser","primaryEmail","siteVerification","6LeIxAcTAAAAAJcZVRqyHh71UMIEGNQ_MXjiZKhI","toast","enableDev",false,"incidentStatus","routes/_layout",{"_15":-5,"_16":17,"_18":17,"_19":11,"_20":11},"username","isAskGordonEnabled",true,"isUsingNewTemplate","showMinimalLanding","showHoneypotTrap","routes/_layout.r.$namespace.$reponame",{"_23":24,"_25":-5,"_26":11,"_27":11,"_28":29,"_30":31,"_32":-5,"_33":11,"_34":35,"_84":-5,"_85":86,"_134":-5,"_135":11,"_136":17,"_137":11,"_138":-5,"_139":140},"canonicalUrl","https://hub.docker.com/r/ymyzk/lambda-rti/tags","mcpServer","canSeeDockerfile","canSeeAutobuilds","namespace","ymyzk","reponame","lambda-rti","cloudBuildSource","isAutobuildsAvailable","repo",{"_36":37,"_38":39,"_41":42,"_43":44,"_45":11,"_46":47,"_48":49,"_50":51,"_53":31,"_28":29,"_54":55,"_56":40,"_57":58,"_59":60,"_61":62,"_63":-5,"_64":58,"_65":66,"_67":11,"_68":29,"_69":70,"_75":11,"_76":77,"_81":29,"_82":83},"categories",[],"content_types",[40],"image","date_registered","2018-02-07T06:15:48.31661Z","description","","is_private","last_updated","2018-10-16T14:28:29.186598Z","last_modified","2024-10-16T13:48:34.145251Z","media_types",[52],"application/vnd.docker.container.image.v1+json","name","pull_count",1249,"repository_type","star_count",0,"status",1,"status_description","active","source","collaborator_count","full_description","# lambda-rti\n\n## THIS PROJECT IS ARCHIVED\nA newer interpreter of the ITGL is available at [ymyzk/lambda-dti](https://github.com/ymyzk/lambda-dti).\n\n[![Build Status](https://travis-ci.org/ymyzk/lambda-rti.svg?branch=master)](https://travis-ci.org/ymyzk/lambda-rti)\n[![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.1186955.svg)](https://doi.org/10.5281/zenodo.1186955)\n\n**lambda-rti** is an interpreter of the implicitly typed gradual language (ITGL).\nThis implementation consists of:\n\n- Garcia and Cimini's type inference algorithm;\n- a cast-inserting translator from the ITGL to the blame calculus; and\n- an evaluator of the blame calculus with runtime type inference.\n\n## Requirements\n- OCaml 4.03.0+\n- Jbuiler (Dune)\n- Menhir\n- OUnit (for running unit tests)\n\n## Getting started\n### Global installation\n```console\n$ dune build\n$ dune install\n$ lrti\n```\n\nRun `$ lrti --help` for command line options.\n\n### Local installation\n```console\n$ dune build\n$ ./_build/default/bin/main.exe\n```\n\nRun `$ ./_build/default/bin/main.exe --help` for command line options.\n\n### Docker\n```console\n$ docker run -it --rm ymyzk/lambda-rti\n```\n\n## Running tests\n```console\n$ dune runtest\n```\n\n## Syntax\n### Top-level\n- Let declaration: `let x ... = e;;`\n- Recursion declaration: `let rec f x ... = e;;`\n- Expression: `e;;`\n\n### Expressions `e`\n- Constants: integers, `true`, `false`, and `()`\n- Unary operators: `+` and `-`\n- Binary operators: `+`, `-`, `*`, `/`, `mod`, `=`, `<>`, `<`, `<=`, `>`, `>=`, `&&`, and `||`\n- Abstraction:\n - Simple: `fun x -> e`\n - Multiple parameters: `fun x y z ... -> e`\n - With type annotations: `fun (x: U1) y (z: U3) ... -> e`\n- Application: `e1 e2`\n- Let expression:\n - Simple: `let x = e1 in e2`\n - Multiple parameters: `let x y z ... = e1 in e2`\n - With type annotations: `let (x:U1) y (z: U3) ... : U ... = e1 in e2`\n- Recursion:\n - Simple: `let rec f x = e1 in e2`\n - Multiple parameters: `let rec f x y z ... = e1 in e2`\n - With type annotations: `let rec f (x: U1) y (z: U3) ... : U = e1 in e2`\n- If-then-else Expression: `if e1 then e2 else e3`\n- Sequence of expressions: `e1; e2`\n- Type ascription: `(e : U)`\n\n### Types `U`\n- Dynamic type: `?`\n- Base types: `bool`, `int`, and `unit`\n- Function type: `U -> U`\n- Type variables: `'a`, `'b`, ...\n\n### Comments\n- Simple: `(* comments *)`\n- Nested comments: `(* leave comments here (* nested comments are also supported *) *)`\n\n## Standard library\nSome useful functions are available:\n```\n# is_bool;;\n- : ? -> bool = \n# is_int;;\n- : ? -> bool = \n# is_unit;;\n- : ? -> bool = \n# is_fun;;\n- : ? -> bool = \n\n# succ;;\n- : int -> int = \n# pred;;\n- : int -> int = \n# max;;\n- : int -> int -> int = \n# min;;\n- : int -> int -> int = \n# abs;;\n- : int -> int = \n# max_int;;\n- : int = 4611686018427387903\n# min_int;;\n- : int = -4611686018427387904\n\n# not;;\n- : bool -> bool = \n\n# print_bool;;\n- : bool -> unit = \n# print_int;;\n- : int -> unit = \n# print_newline;;\n- : unit -> unit = \n\n# ignore;;\n- : 'a -> unit = \n\n# exit;;\n- : int -> unit = \n```\n\n## Examples\n```\n# (fun (x:?) -> x + 2) 3;;\n- : int = 5\n\n# (fun (x:?) -> x + 2) true;;\nBlame on the expression side:\nline 2, character 14 -- line 2, character 15\n\n# (fun (x:?) -> x 2) (fun y -> true);;\n- : ? = true: bool => ?\n\n# (fun (x:?) -> x) (fun y -> y);;\n- : ? = : ? -> ? => ?\n\n# (fun (x:?) -> x 2) (fun y -> y);;\n- : ? = 2: int => ?\n\n# (fun (f:?) -> f true) ((fun x -> x) ((fun (y:?) -> y) (fun z -> z + 1)));;\nBlame on the environment side:\nline 6, character 55 -- line 6, character 69\n\n# (fun (f:?) -> f 2) ((fun x -> x) ((fun (y:?) -> y) (fun z -> z + 1)));;\n- : ? = 3: int => ?\n\n# let id x = x;;\nid : 'a -> 'a = \n\n# let dynid (x:?) = x;;\ndynid : ? -> ? = \n\n# succ;;\n- : int -> int = \n\n# (fun (f:?) -> f 2) (id (dynid succ));;\n- : ? = 3: int => ?\n\n# (fun (f:?) -> f true) (id (dynid succ));;\nBlame on the environment side:\nline 12, character 33 -- line 12, character 37\n\n# let rec sum (n:?) = if n < 1 then 0 else n + sum (n - 1);;\nsum : ? -> int = \n\n# sum 100;;\n- : int = 5050\n\n# sum true;;\nBlame on the expression side:\nline 13, character 23 -- line 13, character 24\n\n# exit 0;;\n```\n\n## References\n- Yusuke Miyazaki. Runtime Type Inference for Gradual Typing. Master's Thesis. Graduate School of Informatics, Kyoto University, 2018.\n- [Ronald Garcia and Matteo Cimini. Principal Type Schemes for Gradual Programs. In Proc. of ACM POPL, 2015.](https://dl.acm.org/citation.cfm?id=2676992)\n","has_starred","hub_user","immutable_tags_settings",{"_71":11,"_72":73},"enabled","rules",[74],".*","is_automated","permissions",{"_78":17,"_79":11,"_80":11},"read","write","admin","user","storage_size",139657744,"orgData","recentTags",[87,124],{"_88":40,"_89":90,"_91":92,"_93":94,"_95":96,"_46":113,"_114":90,"_115":29,"_116":52,"_53":117,"_118":119,"_120":104,"_121":113,"_122":62,"_123":17},"content_type","creator",555417,"full_size",46006196,"id",21878983,"images",[97],{"_98":99,"_100":101,"_102":44,"_103":104,"_105":106,"_107":108,"_109":44,"_110":-5,"_111":92,"_59":62,"_112":-5},"architecture","amd64","digest","sha256:59c20a3a54b25bbb005d75a2f40f7fc25ae3b2f00ca84dac3c7e2f33fc84f006","features","last_pulled","2026-09-07T21:34:17.411170305Z","last_pushed","2018-10-16T14:28:29Z","os","linux","os_features","os_version","size","variant","2018-10-16T14:28:28.827618Z","last_updater","last_updater_username","media_type","latest","repository",3879219,"tag_last_pulled","tag_last_pushed","tag_status","v2",{"_88":40,"_89":90,"_91":125,"_93":126,"_95":127,"_46":132,"_114":90,"_115":29,"_116":52,"_53":133,"_118":119,"_120":130,"_121":132,"_122":62,"_123":17},23158674,23160396,[128],{"_98":99,"_100":129,"_102":44,"_103":130,"_105":131,"_107":108,"_109":44,"_110":-5,"_111":125,"_59":62,"_112":-5},"sha256:ee76ccc2041bb094a8cd1eb7444cd25b1ca95b3800f4f78caf512dadc349d9a5","2026-09-08T03:40:15.425586922Z","2018-03-02T03:09:17Z","2018-03-02T11:26:52.796876Z","v1.1","sbxKitMetadata","isPotentialSpam","isHubSbxKitsEnabled","displaySecurityMetadata","tagAttestations","tagsHaveAttestations",[],"routes/_layout.r.$namespace.$reponame.tags",{"_34":143,"_150":151,"_139":164,"_165":11},{"_36":144,"_38":145,"_41":42,"_43":44,"_45":11,"_46":47,"_48":49,"_50":146,"_53":31,"_28":29,"_54":55,"_56":40,"_57":58,"_59":60,"_61":62,"_63":-5,"_64":58,"_65":66,"_67":11,"_68":29,"_69":147,"_75":11,"_76":149,"_81":29,"_82":83},[],[40],[52],{"_71":11,"_72":148},[74],{"_78":17,"_79":11,"_80":11},"tags",{"_152":153,"_154":-5,"_155":-5,"_156":157},"count",2,"next","previous","results",[158,161],{"_88":40,"_89":90,"_91":92,"_93":94,"_95":159,"_46":113,"_114":90,"_115":29,"_116":52,"_53":117,"_118":119,"_120":104,"_121":113,"_122":62,"_123":17},[160],{"_98":99,"_100":101,"_102":44,"_103":104,"_105":106,"_107":108,"_109":44,"_110":-5,"_111":92,"_59":62,"_112":-5},{"_88":40,"_89":90,"_91":125,"_93":126,"_95":162,"_46":132,"_114":90,"_115":29,"_116":52,"_53":133,"_118":119,"_120":130,"_121":132,"_122":62,"_123":17},[163],{"_98":99,"_100":129,"_102":44,"_103":130,"_105":131,"_107":108,"_109":44,"_110":-5,"_111":125,"_59":62,"_112":-5},[],"canDeleteTags","actionData","errors"]

ymyzk/lambda-rti

Tags for ymyzk/lambda-rti