Eduardo Rafael
Eduardo Rafael
  • 13
  • 45 374

วีดีโอ

What are dependent types? aka the Calculus of Construction (as a type wizard)
มุมมอง 4.1Kปีที่แล้ว
An almost baked video, but now enhanced. Examples shown: github.com/EduardoRFS/youtube-channel/tree/master/19-what-are-dependent-types Yes yes ... wikipedia en.wikipedia.org/wiki/Calculus_of_constructions Social media stuff: www.twitch.tv/eduardorfs TheEduardoRFS
What is a function? aka term abstraction (as a tech youtuber)
มุมมอง 2.8K2 ปีที่แล้ว
Another half baked video, but now enhanced. Wikipedia source as always en.wikipedia.org/wiki/Abstraction_(computer_science) en.wikipedia.org/wiki/Lambda_calculus
How to run code? aka strict evaluation (as a symbol pusher)
มุมมอง 3.9K2 ปีที่แล้ว
This is a bad video, but you know, subscribe and share with your friends. en.wikipedia.org/wiki/Lambda_calculus#Reduction en.wikipedia.org/wiki/Rewriting
Polymorphism on the typed lambda calculus (as a bad chess player)
มุมมอง 2.1K3 ปีที่แล้ว
Mostly we will be talking about System F Introduction to System F and F-Omega by Pablo Nogueira: web.archive.org/web/20210704051919if_/babel.ls.fi.upm.es/~pablo/Papers/Notes/f-fw.pdf Source: github.com/EduardoRFS/youtube-channel/tree/master/14-polymorphism-on-the-typed-lambda-calculus/code
How to write parsers in OCaml using Menhir (as a jedi master)
มุมมอง 3.3K3 ปีที่แล้ว
Well, I'm bad at parsers and also bad at explaining, and this is how this video came to life. Menhir: gitlab.inria.fr/fpottier/menhi Source: github.com/EduardoRFS/youtube-channel/tree/master/13-parser-for-kids-in-ocaml-with-menhir/code
Implementing the simply typed lambda calculus in OCaml (as a not mathematician)
มุมมอง 2.8K3 ปีที่แล้ว
Huge session of recursive types at the end, but that is how coding really is. There is a couple of wrong stuff in this video, but editing it would be painful. Source: github.com/EduardoRFS/youtube-channel/tree/master/12-simple-typed-lambda-calculus-in-ocaml/code
Using postgres with OCaml (as a bad developer)
มุมมอง 2.9K3 ปีที่แล้ว
Huge session of troubleshooting, but that is how coding really is. Source: github.com/EduardoRFS/youtube-channel/tree/master/08-using-postgres-with-ocaml/code ppx_rapper: opam.ocaml.org/packages/ppx_rapper/ examples-reason-postgres: github.com/EduardoRFS/examples-reason-postgres/
How to write an interpreter in OCaml? (as a blockchain developer)
มุมมอง 8K3 ปีที่แล้ว
Source: github.com/EduardoRFS/youtube-channel/tree/master/07-lambda-calculus-interpreter-in-ocaml/code Computerphile video: th-cam.com/video/eis11j_iGMs/w-d-xo.html Lambda Calculus: en.wikipedia.org/wiki/Lambda_calculus
Making a CRUD in OCaml (as a millionaire in Cambodia)
มุมมอง 8K3 ปีที่แล้ว
Source: github.com/EduardoRFS/youtube-channel/tree/master/05-making-crud-in-ocaml/code Opium: opam.ocaml.org/packages/opium Yojson: opam.ocaml.org/packages/yojson/
How to do Higher Kinded Types in OCaml? (as a millionaire in Venezuela)
มุมมอง 3.5K3 ปีที่แล้ว
Source: github.com/EduardoRFS/youtube-channel/blob/master/04-encoding-hkt-in-ocaml/code/hkt.ml Implicits: arxiv.org/pdf/1512.01895.pdf OCaml GADT: ocaml.org/manual/gadts.html OCaml First Class Modules: ocaml.org/manual/firstclassmodules.html

ความคิดเห็น

  • @3ombieautopilot
    @3ombieautopilot หลายเดือนก่อน

    I love your videos! I wish there were more beginner friendly type theory stuff, you explain it so well. Thank you

  • @3ombieautopilot
    @3ombieautopilot หลายเดือนก่อน

    Your videos are more helpful than most articles and papers. Thank you

  • @SB-rf2ye
    @SB-rf2ye 4 หลายเดือนก่อน

    what is your code's colorscheme? it's very pretty.

  • @usercommon1
    @usercommon1 6 หลายเดือนก่อน

    respect

  • @piraloco5864
    @piraloco5864 8 หลายเดือนก่อน

    your screen is so zoomed out i can barely see your bigass forehead

  • @whimahwhe
    @whimahwhe 9 หลายเดือนก่อน

    I'm learning rust and functional programming too and this was really educational, helped me a lot. Thank you, and keep it up!!

  • @nicohussein2635
    @nicohussein2635 9 หลายเดือนก่อน

    Great video man! Do you have some resources that you recommend to dive deeper into these topics? Many thanks!

  • @dmitrijsojma2296
    @dmitrijsojma2296 9 หลายเดือนก่อน

    So, what are the obstacles that make it so hard to implement such a language?

  • @alexpyattaev
    @alexpyattaev 9 หลายเดือนก่อน

    Roc language is essentially rust with implicit refcounting. Except it does away with borrow checking so it feels more like haskell than C.

    • @EduardoRFS
      @EduardoRFS 6 หลายเดือนก่อน

      So it is not essentially rust

    • @alexpyattaev
      @alexpyattaev 6 หลายเดือนก่อน

      @@EduardoRFS well, in most ways it is. It just hides the borrowchecker "under the hood", and when it can not solve the references falls back to refcounting. Rust just forces you to be explicit about the same.

  • @aqua200546
    @aqua200546 9 หลายเดือนก่อน

    I was literally writing "if a tree falls..." just as you said it in the video.

  • @adicide9070
    @adicide9070 9 หลายเดือนก่อน

    rust? you too now? :D

  • @rastrian
    @rastrian 9 หลายเดือนก่อน

    first

  • @bernardoborges8598
    @bernardoborges8598 9 หลายเดือนก่อน

    Have you ever tried Lean Prover?

  • @adicide9070
    @adicide9070 9 หลายเดือนก่อน

    larger font, please, for what it's worth at this point :)

  • @adicide9070
    @adicide9070 9 หลายเดือนก่อน

    this is some good stuff. cool you're using ocaml. hope to see much more of the language out there.

  • @3ombieautopilot
    @3ombieautopilot 10 หลายเดือนก่อน

    Could you recommend a book for beginners on the subject?

  • @texoport
    @texoport 10 หลายเดือนก่อน

    thanks sensei

  • @ga_ts
    @ga_ts 10 หลายเดือนก่อน

    a wild nix user appears

  • @lucaozinho
    @lucaozinho 10 หลายเดือนก่อน

    lgtm

  • @eniebercunha
    @eniebercunha 10 หลายเดือนก่อน

    Heeeee the game change.... welcomen to the nix religion

  • @insertoyouroemail
    @insertoyouroemail 10 หลายเดือนก่อน

    Cool! I'm just a Lisper but I've been thinking about how I could introduce types to my programs.

    • @reycorbie3581
      @reycorbie3581 10 หลายเดือนก่อน

      the little typer/prover

    • @insertoyouroemail
      @insertoyouroemail 10 หลายเดือนก่อน

      @@reycorbie3581 Got both of them! :)

  • @caaltz
    @caaltz 11 หลายเดือนก่อน

    Boaa!

  • @yessure5792
    @yessure5792 ปีที่แล้ว

    good content, thank you

  • @twenty-fifth420
    @twenty-fifth420 ปีที่แล้ว

    I decided for my dream programming language I want dependent types. This video helped me understand further, corrected misunderstandings and made me re-evaluate my perspective. Thank you! Do you have free resources on Coq? The fact it was made in OCaml makes me want to write my language in OCaml but neither her nor there. 😂

  • @kallekula84
    @kallekula84 ปีที่แล้ว

    Which VSCode plugin do you used that gives you inline error messages?

  • @kosnowman
    @kosnowman ปีที่แล้ว

    keep going!

  • @lolifedog1195
    @lolifedog1195 ปีที่แล้ว

    thanks for making this videos. I don't think you are bad a explaining stuff, but if you would slow down a little bit (-0.25) and give more room to what you are saying your message and explanations could come across much clearer.

  • @samuelfreitas5793
    @samuelfreitas5793 ปีที่แล้ว

    Doskya

  • @CodeTalker23
    @CodeTalker23 ปีที่แล้ว

    this guy disappears and then comes back with a banger (btw we need books about these topics to read further)

    • @EduardoRFS
      @EduardoRFS ปีที่แล้ว

      Just because you asked boss. Types and Programming Languages Advanced Topics in Types and Programming Languages Both by Pierce.

  • @rastrian
    @rastrian ปีที่แล้ว

    First

  • @kingivan1151
    @kingivan1151 2 ปีที่แล้ว

    Please do functors

  • @adityapalve3752
    @adityapalve3752 2 ปีที่แล้ว

    This was such a brilliant video Eduardo, absolutely blew my mind!!! thank you

  • @zetaconvex1987
    @zetaconvex1987 2 ปีที่แล้ว

    I guess I'll be the first to address the elephant in the room: what's the deal with the Japanese woman on the pillow?

  • @eventually-consistent
    @eventually-consistent 2 ปีที่แล้ว

    Will `lwt_io` handle data races on the `messages.json` file?

  • @veasnama2136
    @veasnama2136 2 ปีที่แล้ว

    I'm impressed that you're a millioanair in Cambodia by writing Ocaml . Since i just get started learning the language . I am cambodian but we never learn this language in university .

  • @everyhandletaken
    @everyhandletaken 2 ปีที่แล้ว

    Less than 2 minutes into the video & you have created a web server in 2 lines? Did that just happen? You have my attention now!!

  • @daivdninjabiomech7888
    @daivdninjabiomech7888 2 ปีที่แล้ว

    Ocaml witj parsers make me want to kms but props

  • @davisuga
    @davisuga 2 ปีที่แล้ว

    The quality of your videos is constantly increasing, please don't stop with the videos

  • @trejohnson7677
    @trejohnson7677 2 ปีที่แล้ว

    You're such a good backtracking for BIll Evans, I gotta say!

  • @wesleynepomuceno6431
    @wesleynepomuceno6431 2 ปีที่แล้ว

    Brabo!