This presentation was recorded at YOW! 2019. #GOTOcon #YOW https://yowcon.com

Philip Wadler - Professor at University of Edinburgh ‪@philipwadler‬

RESOURCES / philip-wadler-a2bb3a276
https://github.com/wadler https://homepages.inf.ed.ac.uk/wadler https://wadler.blogspot.com

ABSTRACT The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. The proof of a conjunction is a pair, the proof of a disjunction is a case expression, and the proof of an implication is a lambda expression. Proof by induction is just programming by #recursion.

Dependently-typed #ProgrammingLanguages, such as #Agda, exploit this pun. To prove properties of programming languages in Agda, all we need do is program a description of those languages Agda. Finding an abstruse mathematical proof becomes as simple and as fun as hacking a program. This talk introduces Programming Language Foundations in Agda, a new textbook that is also an executable #AgdaScript---and also explains the role Agda is playing in #IOHK's new cryptocurrency. [...]

RECOMMENDED BOOKS Rebecca Skinner • Effective Haskell • https://amzn.to/3SxTpwY Vitaly Bragilevsky • Haskell in Depth • https://amzn.to/3EXpmbe

/ gotocon
/ goto-
/ goto_con
/ gotoconferences
#SoftwareEngineering #Programming #Haskell #SoftwareDevelopmentTutorial #ProgrammingTutorial #FunctionalProgramming #PhilipWadler #YOWcon

Looking for a unique learning experience? Attend the next GOTO conference near you! Get your ticket at https://gotopia.tech Sign up for updates and specials at https://gotopia.tech/newsletter

SUBSCRIBE TO OUR CHANNEL - new videos posted almost daily. https://www.youtube.com/user/GotoConf...

Advait Shinde discusses the history of the theory of computation, delving into axiomatic thinking, Peano axioms, Turing Machines, Lambda Calculus, the Y Comb...

cross-posted from: https://sopuli.xyz/post/10354955

If "category" has a better name....

Isn't it just "composite"?

Every arrow in category can be composed, the set(or class or whatnot..) of that is composite.

cross-posted from: https://sopuli.xyz/post/9969591

Understanding the Type of call/cc

He introduces but also criticizes the use of call/cc, 1. not being a function and looks like a function, 2. able to produce an union of types with it.

Is he correct? What do you think?

I've been enjoying learning ocaml, but I found it very easy to write code riddled with side effects and imperative-ness.

Take this example:

let some_func arg = 
  let input = format_input_from_stdin ()
  let read_content = read_file "some/file/path.txt"
  let to_write = get_write_file_content input read_content
  let () = write_file "some/other/path.txt" to_write 
  let output = run_external_command_with_output 
  (output, read_content)

As you can see, many side effects and imperative steps in the code. Is there a better practice for coding this in a functional manner?

I wanna see what F# is about, especially now that I am better at FP&Lip. But the Microsoft thing really puts me off. I'm on Linux, I can't use CLR, I don't wanna make a WPF application or whatever

so why would I use F#?

I just started to learn Ocaml to learn functional programming. I will use it to build a CLI that's mostly orchestrating other programs.

My experience is mostly in JS / TS, but I've also coded a good bit in Python and Lua.

Below, I provided a list of things I learned or focused on while using OCaml. But I feel like I must be missing something. This is only moderately different from what I'm used to in JS. I expected something more radical. Moreover, I constantly hear a lot of FP jargon (like "highly kinded types", monads, etc) that I feel am still missing.

So far, here's what I studied:

• immutability
• avoid side affects
• static typing
• recursion instead of loops
• option / maybe
• higher order functions
• conditionals and other constructs as expressions, when they're statements in other languages
• pipelines and functions as input —> output
• currying
• scoping with let

What am I missing?

A podcast with transcript which may help explain fp to laymen.

Hello fellow FP-Lemmyites. I'd love to hear stories about what got you interested in FP originally, and how you learned.