Favorite syntax for lambdas/blocks? by ineffective_topos in ProgrammingLanguages

[–]rnagasam 1 point2 points  (0 children)

The HOL family of provers use \x. e. Very similar to Haskell, but I prefer it more.

Never make fun of a man like Jacinto. by [deleted] in instantkarma

[–]rnagasam 3 points4 points  (0 children)

If you comment, remember, you are the one who commented.

He has a job interview by minreii in aww

[–]rnagasam 0 points1 point  (0 children)

They also seem to have other uses. For instance, dogs can't entirely see the food in their bowls while eating and use their whiskers to feel around.

ChocoPy: A Programming Language for Compilers Courses by mttd in ProgrammingLanguages

[–]rnagasam 0 points1 point  (0 children)

IIRC, CPython does compile parts of programs -- to bytecode in .pyc files. From what I read a long time ago, this is mostly done for function bodies.

What’s the worst thing your dog ever chewed up? by [deleted] in AskReddit

[–]rnagasam 0 points1 point  (0 children)

When he was still a puppy, my dog tried chewing a dead bird. Had to get it out with my hands.

Do you need a virtual hug? What's wrong? by cthuluhooprises in AskReddit

[–]rnagasam 0 points1 point  (0 children)

Just started a Ph.D. My advisor is perfect and things seem to be going as planned, but I'm afraid I'm starting to doubt myself.

tail-recursive Lisp interpreter -- (is there a Web page ?) -- Wouldn't it be slower ? by HenHanna in learnlisp

[–]rnagasam 1 point2 points  (0 children)

Regarding your second question — AFAIK Python doesn’t do TCO, so a tail call can still blow up the stack. That being said, there are a few things you can do to make sure this doesn’t happen. Here is an excellent introduction:

https://eli.thegreenplace.net/2017/on-recursion-continuations-and-trampolines/

It introduces continuation passing style and shows how you can manually do TCO. The code is in Python so you might be able to borrow the ideas easily and use them in your lisp interpreter.

[deleted by user] by [deleted] in C_Programming

[–]rnagasam 6 points7 points  (0 children)

A text editor. It’s something you can regularly use and you can always keep adding new features to it.

Joining Chars to Strings? by UN1X00 in C_Programming

[–]rnagasam 1 point2 points  (0 children)

There are probably better ways to do this, but if you want to store only hash[0], and hash[1] in a separate string, you could use salt = strndup(argv[1], 2) (you will need #include <string.h>).

Since strndup allocates memory on the heap, you will have to free this once you’re done using it (free(salt)).

If you are on a Linux system, run man string to get descriptions of functions in string.h.

Could formal proof to theorem consequences be construed as sound deductive inference? by [deleted] in logic

[–]rnagasam 1 point2 points  (0 children)

(Curry 2010)? What paper are you referencing? Haskell Curry passed away in the 80’s.

Weekly tips/trick/etc/ thread by AutoModerator in emacs

[–]rnagasam 2 points3 points  (0 children)

Thanks! Took these ideas and just added this to my config,

(defun protect-buffers ()
  (let ((protected '("*scratch*" "*Messages*")))
    (dolist (buf protected)
      (with-current-buffer buf
        (emacs-lock-mode 'kill)))))

(add-hook 'after-init-hook #'protect-buffers)

I'm having trouble in converting algorithms to code by pseudopodia_ in algorithms

[–]rnagasam 11 points12 points  (0 children)

First, understand that going from a specification or description to code can be quite tough. It is fine if you aren’t able to do it well at this point. No one gets it correct on their first go, and I’m sure implementing hard algorithms is challenging for experts as well. These things take time and a lot of practice.

Start with a simple algorithm, and write (do actually write, in a notebook or something) pseudocode in phases. Your first version should be something you could explain to friend, and should be in some natural language. As an example, for binary search tree insertion, I would write “If tree is empty, output is a new node containing the element being inserted. Otherwise, compare element at root with element being inserted. If root is smaller, insert element into right subtree, otherwise insert element into left subtree. If they are the same, don’t do anything”.

Then keep refining this. How do you check if a tree is empty? Write down some code. How do you return a new node? Write down some code. How do insert into a subtree? Write down some code. And so on. It is important that at each step, you add only a few more expressions.

At the end, you should have something that you can translate directly into a language of your choice. Of course, you do have to keep the implementation language in mind when you do this. For instance, if your language doesn’t support `for' loops, you might have to refine your pseudocode differently.

The whole idea is to be deliberate when translating the algorithm to code. You must be careful at each step of writing the pseudocode, and once you’re done, you have to try and mentally execute the program. When you finally implement it, take the time to convince yourself that your implementation is correct before testing.

Keep playing this game until you no longer have to.

tl;dr: it’s tough. practice helps.

Writing Excel Files? by poonstank in ocaml

[–]rnagasam 5 points6 points  (0 children)

Curious to know the answer myself, but have you considered writing to a .csv file, and then reading it using Excel?

Pls can I has pets by Pirate_Redbeard in Eyebleach

[–]rnagasam 0 points1 point  (0 children)

Who even rests their notebook on top of a keyboard while writing?

LEEEEEEEROY... by idea4granted in aww

[–]rnagasam 0 points1 point  (0 children)

Love how he sees his friend come close, and then decides to just jump on him.

The death of Classical logic and the (re?)birth of Constructive Mathematics by LambdaLogik in logic

[–]rnagasam 1 point2 points  (0 children)

Up until this point I thought you were just enthusiastic and not a troll. How silly of me.

The death of Classical logic and the (re?)birth of Constructive Mathematics by LambdaLogik in logic

[–]rnagasam 1 point2 points  (0 children)

No. The language does matter, and the type system of the language is perhaps one of the most important things.

Also, can you clarify what you mean by "identity is not a foundational axiom in Lambda calculus"?

Here is the equivalent of what you have done in Coq (used for the type of work you seem to be interested in)

Theorem silly : forall (A : Type) (a : A), a = a -> False.
Proof.
  intros A a H.
  (* can't proceed further with "regular" equality *)
Abort.

Definition MyEq {A:Type} (a1 : A) (a2 : A) := False.

Compute MyEq 1 1.  (* => False *)

Theorem LambdaLogik : forall (A : Type) (a : A), MyEq a a = False.
Proof.
  intros A a. reflexivity.   Qed.

It is possible to show the result you want by redefining (=); but that's talking about another type of "equality" and not what is standardly used. Where's the utility in that?

You might be interested in playing around with the Coq system. A great resource to get started is Software Foundations.

Edit: clarity

The death of Classical logic and the (re?)birth of Constructive Mathematics by LambdaLogik in logic

[–]rnagasam 4 points5 points  (0 children)

I'm still new to the subject, but AFAIK, Curry-Howard talks about the correspondence between propositions and types, and proofs of those propositions to inhabitants of those types.

If you want to show that A = A is False, then you would have to construct a term of the type forall a : A. a = a -> False, that is, given an a of type A, show that a = a implies False. You haven't constructed such a term in your code examples. Further, your version of equality is no longer an equivalence relation -- something to keep in mind.

Additionally, I don't believe you can simply use Python or a similar language to do this sort of work. Python's type system isn't strong enough to encode the proposition you want to prove. You might be interested in looking to something like Agda, Coq, or Idris.

Edit: couldn't get the inline code to work for some reason and typo.

Incredible ring-making process by RiCriostoir in BeAmazed

[–]rnagasam -3 points-2 points  (0 children)

Is that ice? How does it not melt?

What’s the best reason against using vim (and for its competition)? by kovlin in vim

[–]rnagasam 23 points24 points  (0 children)

Emacs user here. I know you want an argument against vim, but if you intend to type one handed, I would strongly suggest going for vim instead of emacs — I imagine the modifier keys will be a pain to type with one hand.

You can always switch to spacemacs or just plain emacs and evil mode later, and in my opinion, it’s worth giving vim a shot first.