• R/O
  • HTTP
  • SSH
  • HTTPS

提交

标签
No Tags

Frequently used words (click to add to your profile)

javac++androidlinuxc#objective-cqt誰得windowscocoapythonphprubygameguibathyscaphec翻訳omegat計画中(planning stage)frameworktwittertestdomvb.netdirectxbtronarduinopreviewerゲームエンジン

A categorical programming language


Commit MetaInfo

修订版598d5330e9c6ba9817698d5c44969cbe184cc687 (tree)
时间2022-08-12 10:05:59
作者Corbin <cds@corb...>
CommiterCorbin

Log Message

Okay, well, let's just leave embed/ broken.

更改概述

差异

--- a/embed/embed.ml
+++ b/embed/embed.ml
@@ -1,5 +1,3 @@
1-open Sexplib.Sexp
2-
31 type cammy_prim =
42 | Id
53 | Ignore
@@ -74,15 +72,15 @@ let parse_prim atom =
7472 | "f-atan2" -> Result.ok FATan2
7573 | s -> Result.error ("unknown prim " ^ s)
7674
77-type cammy_functor =
78- | Prim of cammy_prim
79- | Comp of (cammy_functor * cammy_functor)
80- | Pair of (cammy_functor * cammy_functor)
81- | Case of (cammy_functor * cammy_functor)
82- | Curry of cammy_functor
83- | Uncurry of cammy_functor
84- | PR of (cammy_functor * cammy_functor)
85- | Fold of (cammy_functor * cammy_functor)
75+type 'a cammy_functor =
76+ | Prim of 'a
77+ | Comp of ('a cammy_functor * 'a cammy_functor)
78+ | Pair of ('a cammy_functor * 'a cammy_functor)
79+ | Case of ('a cammy_functor * 'a cammy_functor)
80+ | Curry of 'a cammy_functor
81+ | Uncurry of 'a cammy_functor
82+ | PR of ('a cammy_functor * 'a cammy_functor)
83+ | Fold of ('a cammy_functor * 'a cammy_functor)
8684
8785 (* https://okmij.org/ftp/tagless-final/course/final_mod.ml *)
8886 module type CAMMY = sig
@@ -99,7 +97,7 @@ module type CAMMY = sig
9997 end
10098
10199 module Term = struct
102- type repr = cammy_functor
100+ type repr = cammy_prim cammy_functor
103101
104102 let prim f = Prim f
105103 let comp fs = Comp fs
@@ -111,6 +109,55 @@ module Term = struct
111109 let fold fs = Fold fs
112110 end
113111
112+module UglyCulex = struct
113+ type repr = string
114+
115+ let prim f =
116+ match f with
117+ | Id -> "i"
118+ | Fst -> "p"
119+ | Snd -> "q"
120+ | Ignore -> "!"
121+ | Dup -> "n"
122+ | App -> "y"
123+ | Swap -> "x"
124+ | _ -> "."
125+
126+ let comp (f, g) = f ^ g
127+ let pair (f, g) = "<" ^ f ^ "," ^ g ^ ">"
128+ let case (f, g) = "[" ^ f ^ "+" ^ g ^ "]"
129+ let curry f = "^" ^ f
130+ let uncurry f = "v" ^ f
131+ let pr (f, g) = "0" ^ f ^ "1" ^ g
132+ let fold (f, g) = "*" ^ f ^ "++" ^ g
133+end
134+
135+module CurryMap = Map.Make (Int)
136+
137+module type STATEMONAD = sig
138+ type ('s, 'a) t
139+
140+ val return : 'a -> ('s, 'a) t
141+ val bind : ('s, 'a) t -> ('a -> ('s, 'b) t) -> ('s, 'b) t
142+ val get : ('s, 's) t
143+ val set : 's -> ('s, unit) t
144+end
145+
146+module CurryMonad : STATEMONAD = struct
147+ type ('s, 'a) t = 's -> 'a * 's
148+
149+ let return a s = (a, s)
150+
151+ let bind f g s1 =
152+ let a, s2 = f s1 in
153+ g a s2
154+
155+ let get s = (s, s)
156+ let set s _ = ((), s)
157+end
158+
159+open Sexplib.Sexp
160+
114161 module Parser (C : CAMMY) = struct
115162 let rec parse expr =
116163 match expr with
@@ -136,12 +183,53 @@ module Parser (C : CAMMY) = struct
136183 | s -> Result.error "unknown functor" )
137184 end
138185
186+(* https://brianmckenna.org/blog/type_annotation_cofree *)
187+type obj = TN | TV of int | TP of (obj * obj)
188+type polycons = EQC of (obj * obj)
189+
190+module Typer = struct
191+ (* source, target, constraints, next free typevar *)
192+ type repr = int -> (obj * obj * polycons list * int, string) result
193+
194+ let run rep = Result.map (fun (s, t, _, _) -> (s, t)) (rep 0)
195+
196+ let prim f i = match f with
197+ | Id -> let tv = TV i in Result.ok (tv, tv, [], i + 1)
198+ | _ -> Result.error "unknown type"
199+
200+ let comp (f, g) i = Result.error "unknown type"
201+ let pair (f, g) i = Result.error "unknown type"
202+ let case (f, g) i = Result.error "unknown type"
203+ let curry f i = Result.error "unknown type"
204+ let uncurry f i = Result.error "unknown type"
205+ let pr (f, g) i = Result.error "unknown type"
206+ let fold (f, g) i = Result.error "unknown type"
207+end
208+
209+module type FUNCTOR = sig
210+ type 'a t
211+ val map : ('a -> 'b) -> 'a t -> 'b t
212+end
213+
139214 module TermParser = Parser (Term)
215+module CulexParser = Parser (UglyCulex)
216+module TypeChecker = Parser (Typer)
140217
141218 let tree = input_sexp stdin
142-let rep = TermParser.parse tree
219+let rep = CulexParser.parse tree
220+let ty = Typer.run (TypeChecker.parse tree)
143221
144222 let msg =
145- Result.fold ~ok:(fun _ -> "yes parse") ~error:(fun err -> "error: " ^ err) rep
223+ Result.fold
224+ ~ok:(fun s -> "success: " ^ s)
225+ ~error:(fun err -> "error: " ^ err)
226+ rep
227+
228+let tymsg =
229+ Result.fold
230+ ~ok:(fun s -> "success")
231+ ~error:(fun err -> "error: " ^ err)
232+ ty
146233
147-let () = output stdout tree ; print_newline () ; print_endline msg
234+let () = output stdout tree ; print_newline () ; print_endline msg ;
235+print_endline tymsg
--- a/todo.txt
+++ b/todo.txt
@@ -1,3 +1,43 @@
1+* DAG of compiler stages
2+ * Pipedreams
3+ * Cammy -> GLSL
4+ * Would allow GPU rendering
5+ * Monte B. -> Cammy
6+ * Completes the dream of making Monte fast
7+ * Cammy -> Elm
8+ * Would maybe be a path to browser support
9+ * Cammy -> Haskell
10+ * Why?
11+ * Former stages
12+ * Cammy -> OCaml
13+ * Was important for bootstrapping
14+ * Could still be a decent general-purpose target
15+ * Cammy -> Scheme
16+ * Dire mismatch in typing discipline
17+ * CHICKEN Scheme can compile point-free expressions well
18+* Ordinal types
19+ * 1, 2, 3, ..., N
20+ * No 0, because no way to construct it, so no meaningful usage
21+ * New type-inference constraint: (lte X Y) or (lt X Y)
22+ * Every ordinal is equal to itself: (lte 1 1), (lte 2 2), ..., (lte N N)
23+ * Every ordinal is less than N: (lt 1 N), (lt 2 N), etc.
24+ * Generalized zero : 1 -> X, (lte X N)
25+ * Generalized succ : X -> Y, (lt X Y)
26+ * Maybe instead have a new typevar 'Ord
27+ * zero : 1 -> Ord(X)
28+ * succ : Ord(X) -> Ord(Y), (lt X Y)
29+ * Generalized (specialized?) primitive recursion
30+ * pr : Ord(X) -> Y, given 1 -> Y, Y -> Y
31+ * To still be able to infer Ord(X) ~ N, would require noticing (lt X N)
32+ situations and widening X correctly when extracting types
33+ * Use cases
34+ * Generalized matrices: Ord(X) × Ord(Y) -> F is like an X×Y matrix
35+ * Polynomial functors: X² + X + 1 can literally be encoded as:
36+ * X -> [2, X] + (X + 1)
37+ * So we could generalize that to any ordinal
38+ * Perhaps generate monad instances automatically?
39+ * Basic enums, for better sum types
40+ * Haskell-style ADTs are basically polynomial functors
141 * REPL improvements
242 * : commands
343 * help, describe commands
@@ -47,6 +87,7 @@
4787 * We'd need an equivalence X × 1 → X
4888 * swap and dup would need to be primitive again too
4989 * Prove that nat/add is smallest with its behavior
90+ * Would justify its jet, since no smaller expression could be jetted
5091 * Streams
5192 * Monad: X → [N, X]
5293 * Special case of reader monad
@@ -103,11 +144,6 @@
103144 * https://okmij.org/ftp/continuations/undelimited.html
104145 * It's about time to rewrite the multisampling logic in Cammy
105146 * Mostly just needs pixel radius to be passed to image
106-* Some basic dependent types
107- * Type-level arithmetic would be nice
108- * Could have types like (fin n): not just 1 and 2, but 3, 4, etc.
109- * Also generalized tensors: vectors are (gt n), matrices are (gt m n),
110- tensors are (gt l m n), etc.
111147 * Use Elliott's techniques to compile to a graph?
112148 * And then display the graph!
113149 * Zippers http://strictlypositive.org/diff.pdf