monads help

Stream: new members

[Simon Daniel]

i try to describe a dependent type that only lives inside a monadic application similar to

inductive depType: Nat -> Type

def fn: Reader Nat Unit := do
  let state <- read
  let v: depType state := sorry -- should implicetly depend on state
  return ()

but depType should be only accessible from within the monad and depend on the reader state. Is that even possible?

[Matt Diamond]

the Reader monad doesn't have state (the input is read-only)... there are other monads (like the State monad) that do

[Simon Daniel]

hmm i want the state to be read only (correct me if state is not the correct term without mutability)
maybe this helps to clarify

-- I want to run this in a Reader monad such that depType uses the reader State instead of SomeNat
def use_wantedType (v: depType some_Nat): ReaderM Nat Unit := do
  let state <- read
  let wantedType := depType state
  -- i want this v: wantedType
  return ()

[Simon Daniel]

it would be a function like

def wantedType: ReaderM Nat (Type) := do
  let state <- read
  return depType state

which seems impossible. But maybe im missing something

[Mario Carneiro]

You may need to just write it as a dependent function instead of using ReaderM sugar

[Mario Carneiro]

but you haven't really given a complete #mwe here, only fragments which don't really fit together into a program. How are you going to create an element of depType state? What do you want to do with the result?

[Mario Carneiro]

What is some_Nat here, and how does it relate to the value in the reader monad? The problem is that you have two values being passed into the function and your "I want this" is implicitly asserting that they are the same but there is no reason for them to be

[Simon Daniel]

okay here a more complete example of what im currently doing

inductive Loc
| alice | bob
deriving DecidableEq
open Loc

inductive GVal (owner endpoint: Loc) (α: Type)   where
| Wrap:  (owner = endpoint) -> α -> GVal owner endpoint α
| Empty: (owner ≠ endpoint) -> GVal owner endpoint α

-- creates a GVal at loc using IO
def create_val (loc ep: Loc) (comp: α): IO (GVal loc ep α) := do
if h:( loc = ep) then
    return GVal.Wrap h (comp)
  else
    return  GVal.Empty h

def send_val (l1 l2 ep: Loc) (v: GVal l1 ep α) : IO (GVal l2 ep α) :=
  sorry -- Wraps an α if ep = l2, otherwise .Empty

def someProg (ep: Loc): IO Unit := do
  let v <- create_val Loc.alice ep 2
  let v2 <- send_val alice bob ep v
  return ()

[Simon Daniel]

my problem is that inside someProg the (ep:Loc) should be passed along implicetely. But when i do with a Reader it seems like i have to erase the endpoint from GVal and loose the proof that (owner = endpoint) implies a .Wrap