eiurafhlfie

I'll remember to never sign up for that service. Thank you.

Tagged union types (called `enum` in Rust), recursion, and pattern matching are great for tree data structures, such as ASTs, and help catch many bugs. This is the reason why so many compilers, typecheckers, and interpreters are written in languages like OCaml, F#, Haskell, and Rust.

Beautiful! Also, nice website.

Bear in mind though that Ebay Japan does not target EU/no/ch customers, which is a requirement for the "big reach" of the GDPR.

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...

Thanks for your reply.

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"

You are correct about what `(k_intint (Int 1))` should be. I hope for `k_intint` to be `IntTy -> IntTy -> IntTy`.

Hi Hacker News PL enthusiasts. This is off topic, but I hope you will have mercy on me.

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))

If you are middle class (~$30k-$70k per annum) you can be wealthy* by focusing your spending on freedom, aka capital investments. I did not understand this was an option before reading the blog of Mr. Money Mustache[0]. Reading that and the Living a FI blog[1] may hopefully be as life-changing to you reading this comment as it was for me.

* Wealthy in time to spend with those you love

[0] https://www.mrmoneymustache.com/

[1] https://livingafi.com/

> 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 :-)

Think it's very rare here. I certainly did realize those things before listening to Jordan Peterson's lectures on Genesis.

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'm a native of Sweden, a secular protestant Christian country. In my understanding of the world, the Christian way of seeing the world stems from the Greek philosophers mainly, among others.

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.

I've made the same observation traveling in poor and rich countries. Corruption is Α & Ω. It is everyone's responsibility to not parttake in it. It seems to me that lying (using The Word, logos, in untruthful ways) and corruption (using your power in untruthful ways) are the most unholy sins.

One more bitcoin bubble poppin'.

Does HN think it's the last one, or will the pattern repeat in a few years again?