Conversation

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Apr 28, 2021

Something that came up on the /r/ProgrammingLanguages Discord when I posted this: could you avoid adding the monad if you didn't have effects (like mutable refs in ML)? Ie. just use lambda parameters as a way of doing abstraction?

Brendan Zabarauskas

@brendanzab

Apr 28, 2021

The example that was given was: (λ(m1 : M) (m2 : M). body) m m which emulates: let m1 : M ← m m2 : M ← m in body where `copy1 ≠ copy2`? Or is there some other use for the monad that I might be missing?

Replying to

and

I'm not sure how hard that translation is in practice though. One example where a I thought monad might be handy was having nominal datatypes without relying on a top-level command language, but I'm not sure if this could be done with lambdas too.

2:15 AM · Apr 28, 2021Twitter Web App

Replying to

and

Perhaps doing this with lambdas could allow for cool metaprogramming possibilities?

Brendan Zabarauskas

@brendanzab

Apr 28, 2021

I think Conor Mcbride talked about using natural numbers for datatype ids in his talk on Epigram 2 (it came up in a question, but I forget the timestamp): vimeo.com/428161108 - not sure what the implications are for implementation hiding and abstraction though.

vimeo.com

Conor McBride: Epigram 2 - Autopsy, Obituary, Apology

Seminar for foundations of mathematics and theoretical computer science Faculty of Mathematics and Physics, University of Ljubljana EPIGRAM 2: AUTOPSY, OBITUARY,…

Show replies