Readit NewsLet me know if anyone wants me to open source this :)
Wikipedia excerpt: "... for all individuals within the European Union (EU) and the European Economic Area (EEA)."
https://en.wikipedia.org/wiki/General_Data_Protection_Regula...
Just fyi, this is called System F.
I do not remember any OCaml and I get an error when trying to run it (File "./test.ml", line 123, characters 6-7: Error: Syntax error: operator expected.) so I do not know if I can be of much help. What is the result of typ_of_expr [] (app k_intint (Int 1))? I presume that you expect it to be IntTy -> IntTy, right?
It is indeed system F I'm trying to implement :-)
My formatting for HN seems to have screwed the program up. You'll find the contents of systemf.ml in this paste: https://pastebin.com/gw20LBNR
Here is the result from my OCaml repl:
# typ_of_expr [] (app k_intint (Int 1));;
- : (typ, string) result =
Error "Type mismatch. t0_0: SymbolTy a, t0_1: Arrow, t1: IntTy"
I'm reaching out for some help from you. I've been working on interpreters this whole year, taking on no more work for pay than needed for rent and food, so that I can realize my programming language dream. I'm writing a couple of interpreters every week, trying out new ideas. But there is one hurdle I've been unable to overcome for a long time.
I'm trying to write a typechecker for a simple lambda calculus with polymorphic functions. My acceptance criteria is being able to typecheck the K combinator. I've been stuck at this point for months. Have read all I can find on the internet, and have read TAPL many times.
Am honestly feeling really stupid for not having been able to complete this.
What I'm struggling with beta reducing expressions that are type lambdas (i.e. the expression related to `Forall`).
Λ means type lambda, i.e. the set of expressions indexed by type
λ means expression lambda, i.e. the set of expressions indexed by expression
E.g. Λa.λx:a.x is the polymorphic "identity" function, which in javascript looks like `x => x`
k = ΛA.ΛB.λx:A.λy:B.x
k_intint = ((k IntTy) IntTy)
What I have yet been unable to do is type_of k_intint, and this because beta reduction should return an expression, but type_of should return a type.
I'll paste the source code of my latest attempt below, the function in question is `typ_of_expression`. I've written this in OCaml, but would be very thankful for a response in any language, or pseudocode, or just explained in English.
Many thanks for taking the time to read this. For any reply or pointer in the right direction I would be greatly thankful. You know what, I'd be happy to pay €100 for any help that lets me solve this (SEPA, Bitcoin).
(* λ calculus, with Forall and simple types *)
type 'a binding =
| SymBind of 'a
| QuantifierBind
type 'a context = (string * 'a binding) list
type typ =
| UnitTy
| IntTy
| Arrow of typ * typ
| Forall of string * typ
(* Thought it simpler to separate Closure and Lambda, for w hen I later add records/unions etc *)
| ClosureTy of (typ context) * typ
| SymbolTy of string
type expr =
(* again thought it simpler to separate Closure and Lambda, for when I later add records/unions etc *)
| Closure of (expr context) * expr
| Unit
| Symbol of string
| Int of int
| Lam of string * typ * expr (* turns into Arrow. Takes ex pr as argument, returns expr *)
| App of expr * expr
| TLam of string * expr (* expr version of Forall. Ta kes typ as argument, returns expr *)
| TApp of expr * typ
let rec lookup context key =
match context with
| [] -> Error "No result"
| (k, QuantifierBind) :: rest -> lookup rest key
| (k, SymBind v) :: rest -> if key = k
then Ok v
else lookup rest key
let str = String.concat ""
let rec string_of_typ t = match t with
| UnitTy -> "UnitTy"
| IntTy -> "IntTy"
| Arrow _ -> "Arrow"
| Forall (s, t) -> str ["Forall "; s; " "; string_of_typ t]
| ClosureTy (_ctx, t) -> str ["Closure "; string_of_typ t]
| SymbolTy s -> str ["SymbolTy "; s]
let string_of_expr e = match e with
| Unit -> "Unit"
| Closure _ -> "Closure"
| Symbol s -> str ["Symbol "; s]
| Int i -> str ["Int "; string_of_int i]
| Lam _ -> "Lam"
| App _ -> "App"
| TLam _ -> "TLam"
| TApp _ -> "TApp"
(* Convert between context types, such as (expr context) or ( typ context) *)
let rec convert_context converter_fn original_context exprcon text acc = (* カリたべたい *)
let convert_context = convert_context converter_fn original _context in
match exprcontext with
| [] -> acc
| (x, QuantifierBind) :: rest ->
convert_context rest ((x, QuantifierBind) :: acc)
| (x, SymBind e) :: rest ->
(match converter_fn original_context e with
| Ok t -> convert_context rest ((x, SymBind t) :: acc)
| Error e -> failwith (str ["typ_context error: "; e]))
let rec typ_of_expr context e =
match e with
| Unit -> Ok UnitTy
| Int i -> Ok IntTy
| Closure (ctx, e) ->
let new_context = convert_context typ_of_expr context ct x context in
typ_of_expr new_context e
| Symbol s -> lookup context s
| Lam (x, in_typ, body) ->
(let new_context = (x, SymBind in_typ) :: context in
match typ_of_expr new_context body with
| Ok return_typ -> Ok (Arrow (in_typ, return_typ))
| Error e -> Error (str [ "Error finding return type of lambda. Error: "
; e]))
| App (e0,
e1) ->
(match (typ_of_expr context e0,
typ_of_expr context e1) with
| (Ok (Arrow (t0_0, t0_1)),
Ok t1) -> if t1 = t0_0
then Ok t0_1
else Error (str ["Type mismatch"])
| (Ok (ClosureTy (ctx, Arrow (t0_0, t0_1))),
Ok t1) -> if t1 = t0_0
then Ok t0_1
else Error
(str
["Type mismatch. t0_0: "
;string_of_typ t0_0
;", t0_1: "
;string_of_typ t0_1
;", t1: "
;string_of_typ t1
])
| (Ok t, _) -> Error (str ["Not given a lambda as first thing to App. "
;string_of_typ t])
| _ -> Error (str ["Error getting typ of expr App"]))
| TLam (a, body) ->
(let new_context = (a, QuantifierBind) :: context in
match typ_of_expr new_context body with
| Ok body_type -> Ok (ClosureTy (new_context,
Forall (a,
body_type)))
| Error e -> Error (str [ "Failed to get typ of TLam, a nd thus can not construct Forall. Error: "
; e]))
| TApp (TLam (a, body),
t1) -> let new_context = (a, QuantifierBind) :: con text in
typ_of_expr new_context body
| TApp (e0, t1) ->
(match typ_of_expr context e0 with
| Ok (ClosureTy (ctx,
Forall (a, body))) ->
let new_context = (a, SymBind t1) :: ctx @ context i n
Ok (ClosureTy (new_context,
body))
| Ok (ClosureTy(ctx,
t)) ->
Error (str ["TApp given ClosureTy with non-forall on left-hand-side. IS: "
;string_of_typ t])
| Ok (Forall (a, body)) -> Error "TApp given naked Fora ll as first argument"
| Ok _ -> Error "TApp given non-Forall first argument"
| Error e -> Error (str ["Error in TApp - error: "
;e]))
let rec eval context e =
let context: (expr context) = context in
match e with
| Unit -> Ok Unit
| Closure (ctx, e) -> eval (List.append ctx context) e
| Int i -> Ok (Int i)
| Lam (x, t, body) -> Ok (Closure (context,
Lam (x, t, body)))
| Symbol s -> lookup context s
| App (Closure(ctx,
Lam (x, t, body)),
e1) ->
let new_context = (x, SymBind e1) :: ctx @ context in
eval new_context body
| App (e0, e1) ->
(match eval context e0 with
| Ok (Closure (ctx,
Lam (x, t, body))) ->
eval (ctx @ context) (App (Lam (x,
t,
body),
e1))
| Ok _ -> Error "Can't apply non-Lam"
| Error e -> Error (str ["Apply error: "
;e]))
| TLam (a, body) -> Ok (TLam (a, body))
| TApp (TLam (a, body),
given_typ) ->
let new_context = (a, QuantifierBind) :: context in
eval new_context body
| TApp (e0, t) ->
(match eval context e0 with
| Ok (TLam (a, body)) ->
let _ = failwith "Not gonna happen" in
eval context (TApp (TLam (a, body), t))
| Ok (Closure (ctx,
TLam (a,
body))) ->
eval (ctx @ context) body
| Ok _ -> Error "Can't type-apply non-Λ"
| Error e ->
Error (str [ "Error applying type lambda. Error: "
; e]))
(* helper functions *)
let tlam a body = TLam (a, body)
let lam x t body = Lam (x, t, body)
let app e0 e1 = App (e0, e1)
let tapp e0 tyT1 = TApp (e0, tyT1)
(* eval [] (tlam "a" (lam "x"
* (SymbolTy "a")
* (Symbol "x"))) *)
let k_combinator = (tlam "a" (tlam "_b"
(lam
"x"
(SymbolTy "a")
(lam
"_y"
(SymbolTy "_b")
(Symbol "x")))))
let k_intint = (TApp (TApp (k_combinator,
IntTy),
IntTy))
(* DEAR HN READER: This is what is failing me. *)
let applied_k = typ_of_expr [] (app k_intint (Int 1))* Wealthy in time to spend with those you love
Personally, I've mainly heard Logos and "The Word" in the context of kinda borderline esoteric christians or sufi's like Rudolf Steiner, Gurdjieff or Gnosticism in general, etc. Which I guess makes sense considering they all share an appreciation of christian knowledge, language and understanding.
And definitely take notes while high! I honestly couldn't recommend it enough. I'm not sure if you read that Carl Sagan quote in my previous comment but it described it very well. The simple act of writing down the idea solidifies it and makes it more permanent... sort of anchors it in existence (where before it is more ephemeral), allowing you to refer to it again in the future. I always found it immensely relieving to know that I have written down an idea because then I don't need to think of it anymore and can let it go, knowning that it's effectively been internalized and will eventually come back to me with new inspiration.
The funny thing is that I've almost never read any of my notes, but the simple psychological comfort of knowing that I Could, and that my ideas are safely externalized and a history of them is relatively incorruptible... is profoundly comforting and ultimately, I believe, is what has enabled my ideas to evolve very rapidly. It's my belief that the simple act of writing notes while you're high seems to create a powerful internal psychological foundation for the rapid evolution of ideas.
And thanks for the invite! Likewise, if you're ever around Montreal or Toronto, drop me a line
Duuuuude(gender neutral)!!! I love going to Toronto and Montreal both! A very good friend of mine is Torontian, and I've spent a lot of time there and around Ontario and Quebec.
My Bitmessage address is in my HN profile description, feeling uneasy about publishing my email publicly.
> Personally, I've mainly heard Logos and "The Word" in the context of kinda borderline esoteric christians or sufi's like Rudolf Steiner, Gurdjieff or Gnosticism in general, etc. Which I guess makes sense considering they all share an appreciation of christian knowledge, language and understanding.
Then, let's take the word "The Word" back :-)
How about yourself? What's your take on those things?
Read some of your comments, totally gonna start carrying a notebook when using weed. You seem like a nice person, feel free to drop me a line if visiting the Scandinavia.
I think it's true that the prosperity of my corner of the world (including the non-European western nations too) is rooted in holding "The Word", logos, in the highest regards, even if I don't hold any metaphysical beliefs.
The other day I tried to delete my udacity account. No button in settings, I mailed support, they asked my to mail legal (apparently they don't fwd mail..). From legal I received the following response:
Hello,
We are in receipt of your request to delete your account. We are sorry you want to leave the Udacity family; you will be missed.
Before we can proceed with fully processing your request, we need to verify your information. We take these steps to minimize risk to the security of your information and of fraudulent information and removal requests. Specifically, we ask that you provide the following pieces of information:
- Username and email address associated with your Udacity User Account (if different from the one you provided in your initial request);
- Online Courses currently or previously enrolled in;
- Approximate date of User Account registration;
- Country of residence; and
- A statement under penalty of perjury that all information in your request is truthful and that this is your User Account or that you have the authorization to make the request on behalf of the owner of the User Account.
If, after you have provided the above information, we are unable to verify your identity and/or authority to issue the request, we may reach out to you for further verification information.
As a reminder, any deletion actions we take in response to your request are not reversible and may result in Udacity (or you) being unable to retrieve information about your account, enrollment, and records of completion. Please also keep in mind that all removals of such information are subject to requirements to maintain certain data in our archives for legal or legitimate business purposes.
If you have any questions about this request please see our Privacy Policy or let us know.
Thanks for your understanding.
Udacity Legal Team