Conversation

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Brendan Zabarauskas
@brendanzab
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?
2
3
Brendan Zabarauskas
@brendanzab
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?
1
Brendan Zabarauskas
@brendanzab
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.
1
Brendan Zabarauskas
@brendanzab
Replying to
@brendanzab
and
@jonmsterling
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,…
Twitter Web App
András Kovács
@andrasKovacs6
Replying to
@brendanzab
and
@jonmsterling
I think that's more about making type functions injective wrt type inference, so that e.g. Functor C D = Functor C' D' implies C = C' and D = D' (= is definitional). With fully structural records, inference too often fails bc of lack of injectivity. It doesn't hide info though
3