Modeling la monade ST in Agda

Question

Questa recente SO question mi ha spinto a scrivere un'emulazione non sicura e pura della monade ST in Haskell, una versione leggermente modificata di cui potete vedere qui sotto:

{-# LANGUAGE DeriveFunctor, GeneralizedNewtypeDeriving, RankNTypes #-} 

import Control.Monad.Trans.State 
import GHC.Prim (Any) 
import Unsafe.Coerce (unsafeCoerce) 
import Data.List 

newtype ST s a = ST (State ([Any], Int) a) deriving (Functor, Applicative, Monad) 
newtype STRef s a = STRef Int deriving Show 

newSTRef :: a -> ST s (STRef s a) 
newSTRef a = ST $ do 
    (env, i) <- get 
    put (unsafeCoerce a : env, i + 1) 
    pure (STRef i) 

update :: [a] -> (a -> a) -> Int -> [a] 
update as f i = case splitAt i as of 
    (as, b:bs) -> as ++ f b : bs 
    _   -> as 

readSTRef :: STRef s a -> ST s a 
readSTRef (STRef i) = ST $ do 
    (m, i') <- get 
    pure (unsafeCoerce (m !! (i' - i - 1))) 

modifySTRef :: STRef s a -> (a -> a) -> ST s() 
modifySTRef (STRef i) f = ST $ 
    modify $ \(env, i') -> (update env (unsafeCoerce f) (i' - i - 1), i') 

runST :: (forall s. ST s a) -> a 
runST (ST s) = evalState s ([], 0) 

Sarebbe bene se potessimo presentare la solita API monad ST senza unsafeCoerce. In particolare, mi piacerebbe formalizzare le ragioni per le quali funziona la solita monade GHC ST e l'emulazione di cui sopra. Mi sembra che essi funzionano perché:

• Qualsiasi STRef s a con il diritto s tag deve essere stato creato nella corrente calcolo ST, dal momento runST assicura che diversi stati non possono essere scambiati.
• Il punto precedente insieme al fatto che i calcoli ST possono solo estendere l'ambiente dei riferimenti implica che qualsiasi STRef s a con il tag s corretto fa riferimento a una posizione valida nell'ambiente (a) (dopo aver eventualmente indebolito il riferimento in fase di esecuzione) .

I punti sopra riportati consentono un'esperienza di programmazione notevolmente esente da prove. Niente si avvicina davvero in Haskell puro e sicuro a cui possa pensare; possiamo fare un'imitazione piuttosto scadente con le monade di stato indicizzate e le liste eterogenee, ma questo non esprime nessuno dei punti precedenti e quindi richiede prove per ogni sito d'uso di STRef-s.

Non riesco a capire come potremmo formalizzarlo correttamente in Agda. Per i principianti, "assegnato nel questo calcolo" è abbastanza complicato. Ho pensato di rappresentare STRef -s come prova che una particolare allocazione è contenuta in un particolare calcolo ST, ma ciò sembra comportare una ricorsione infinita di tipo indexing.

Answer 1

Ecco una qualche forma di soluzione fatta postulando un teorema di parametricità. Garantisce inoltre che il postulato non interferisca con il calcolo.

http://code.haskell.org/~Saizan/ST/ST.agda

"darcs ottenere http://code.haskell.org/~Saizan/ST/" per la sorgente completo

io non sono contento del universo chiuso di tipi ma è il modo più semplice per personalizzare il teorema parametricity a quello che abbiamo effettivamente bisogno.