chris martensdo yall have any favorite papers that say useful things about what “domain specific languages” are/are for/if the concept even makes any sense/etc
i have a fresh no-context take that imperative programming is a DSL
jcreed@chrisamaphone I mean... strong agree? this is how it feels in Lean and it's quite pleasant. "Wanted to update locally mutable variables anyway for a laugh? We had a tool for that: It was called "DO NOTATION OVER THE IDENTITY MONAD" "
Lindsey Kuper@jcreed @chrisamaphone yeah, I mean, "monads are DSLs" is a venerable and useful take
@chrisamaphone @jcreed I'm not talking about any particular "general-purpose" language either, just observing that "oh, you want to mess with state or control flow? there's a little language for that" is an attested phenomenon
@chrisamaphone like, genuine question, I don't know haskell's whole feature set, can you do like
def look_no_state_monad (n gas : Nat) : Id Bool := do
let mut n := n
let mut gas := gas
while gas > 0 do
if n == 1 then return true
if n % 2 == 0
then n := n / 2
else n := 3 * n + 1
gas := gas - 1
dbg_trace n
return false
/--
info: 53
---
info: false
-/
#guard_msgs in
#eval look_no_state_monad 27 100
/-- info: true -/
#guard_msgs in
#eval look_no_state_monad 27 200
@jcreed i’m not sure i understand the question (what’s going on with the stuff at the bottom? what source language is this?) but also i almost certainly also don’t know more about haskell than you do
@jcreed nm i think i understand the intent of your code but i still don’t know what you’re asking about haskell, like does it have something analogous to := and mut? without desugaring to the state monad? i dont think so?
@chrisamaphone yeah, the Lean feature I found exciting (but I'm aggressively trying to rhetorically cover my butt because I don't actually know if it's novel to Lean but it might be?) is that you can write muts and loops in do notation even in the identity monad, and it desugars them away and this is really nice.
@chrisamaphone And I felt that it aligned very strongly with your sentiment of "imperative programming, what's the big deal, it's just a DSL". It is in Lean literally a DSL that any library author could have implemented. It barely even engages with the monad machinery from the point of view of the user of it: I gotta say "Id" but that's it, Id Bool and Bool are definitionally equivalent. When I call look_no_state_monad I don't need to invoke .run or anything to "bring it back from monad world"
Philippa Cowderoy@jcreed @chrisamaphone I'd rather an
Id run call around the edges myself normally (or possibly a do Id) not least because unless you're trying to weaken to it the identity monad may as well be any monad. But this is partly a "typeclasses being awkward" thing coupled with me being effect-happy.
Kaustuv Chaudhuri@jcreed @chrisamaphone Haskell doesn't have nonrecursive lets, so you can't even manually desugar the "let mut" and ":=" yourself without tedious bookkeeping of variable versions.
@jcreed @chrisamaphone I would legit rather have good syntax for unfolds/anamorphisms, though I appreciate Lean probably shouldn't do loops that way!
(I once pushed a list reversal written as a fold through the initial algebra/final coalgebra isomorphism, and by far the hardest bit was not having neat labels for what the seed -> (cons * seed + nil) function was doing in terms of the coalgebra)
alecsdef look_no_state_monad : Nat → Nat → Id Bool :=
fun n gas =>
have n := n;
have gas := gas;
do
let r ←
forIn Lean.Loop.mk ⟨none, gas, n⟩ fun x r =>
have r := r.snd;
have gas := r.fst;
have n := r.snd;
if gas > 0 then
have __do_jp := fun gas n y =>
have __do_jp := fun gas n y =>
have gas := gas - 1;
do
pure PUnit.unit
pure (ForInStep.yield ⟨none, gas, n⟩);
if (n % 2 == 0) = true then
have n := n / 2;
do
let y ← pure PUnit.unit
__do_jp gas n y
else
have n := 3 * n + 1;
do
let y ← pure PUnit.unit
__do_jp gas n y;
if (n == 1) = true then pure (ForInStep.done ⟨some true, gas, n⟩)
else do
let y ← pure PUnit.unit
__do_jp gas n y
else pure (ForInStep.done ⟨none, gas, n⟩)
match r.snd with
| ⟨gas, n⟩ =>
have __do_jp := fun y => dbgTrace (toString n) fun x => pure false;
match r.fst with
| none => do
let y ← pure PUnit.unit
__do_jp y
| some a => pure a
In the end it looks a lot like the state monad anyway
@bool @chrisamaphone right, after being desugared, exactly
@jcreed @chrisamaphone nope, using references to mutable cells is syntactically chonky and there's no room to pun
the state monad doesn't give you references, instead it gives you get/set and interderivable operations on a single mutable cell - plays nicely with lenses though and as it's Just Ordinary Code you can use lenses to use part of the outer cell as your locally relevant cell
no syntactic support for looking like imperative code rather than code with some sequencing though
none of which stopped lennart augustsson from embedding a line-numbered basic into it for the hell of it
David Young@jcreed @chrisamaphone No, the only "magic" that happens with monads in Haskell is the desugaring of do notation into applications of >>=.
What you're describing would need a little more magic than that.