io - Agda: Lectura de una línea de entrada estándar como una cadena en lugar de un Costring

Question

Intento escribir un programa simple que lea una línea de entrada estándar, la invierta y luego imprima la cadena invertida.

Desafortunadamente, la función nativa getLine lee un Costring ; Solo puedo revertir String s; y no hay ninguna función que lleve un Costring a una String .

¿Cómo puedo modificar este programa para compilar?

module EchoInputReverse where

-- Agda standard library 0.7
open import Data.List using (reverse)
open import Data.String
open import Foreign.Haskell using (Unit)
open import IO.Primitive

postulate
  getLine : IO Costring

{-# COMPILED getLine getLine #-}

main : IO Unit
main = 
  getLine >>= (λ s → 
  -- NOTE: Need a (toString : Costring → String) here. Or some other strategy.
  return (toCostring (fromList (reverse (toList (toString s))))) >>= (λ s'' → 
  putStrLn s''))

Answer 1

No puedes hacer eso, al menos no directamente. El problema es que Costring puede tener un tamaño infinito, mientras que String s debe ser finito.

Imagine ejecutar el programa como prog < /dev/zero , ¿qué debería pasar? La función reverse puede producir el primer elemento solo después de llegar al final de la lista de entrada y es posible que nunca ocurra.

Necesitamos expresar el hecho de que la conversión de un Costring a String puede fallar. Una forma de hacerlo es usar la mónada de parcialidad. Echemos un vistazo a la definición:

data _⊥ {a} (A : Set a) : Set a where
  now   : (x : A) → A ⊥
  later : (x : ∞ (A ⊥)) → A ⊥

Entonces, podemos tener un valor de tipo A este now , o tenemos que esperar later . Pero observe el símbolo:: eso significa que realmente podemos esperar para siempre (ya que puede haber un número infinito de constructores later ).

Combinaré la conversión y la inversión en una función. Importaciones primero:

open import Category.Monad.Partiality
open import Coinduction
open import Data.Char
open import Data.Colist
  using ([]; _∷_)
open import Data.List
  using ([]; _∷_; List)
open import Data.String
open import Data.Unit
open import IO

Ahora, el tipo de nuestra función reverse debe mencionar que tomamos un Costring como entrada, pero también que devolver una String puede fallar. La implementación es bastante simple, es la inversión habitual con el acumulador:

reverse : Costring → String ⊥
reverse = go []
  where
  go : List Char → Costring → String ⊥
  go acc []       = now (fromList acc)
  go acc (x ∷ xs) = later (♯ go (x ∷ acc) (♭ xs))

Sin embargo, podemos imprimir una String , pero no una String ⊥ ! Ahí es donde IO ayuda: podemos interpretar los constructores later como "no hacer nada" y si encontramos now constructor, podemos putStrLn String la String que contiene.

putStrLn⊥ : String ⊥ → IO ⊤
putStrLn⊥ (now   s) = putStrLn s
putStrLn⊥ (later s) = ♯ return tt >> ♯ putStrLn⊥ (♭ s)

Tenga en cuenta que utilizo el IO del módulo IO , no el de IO.Primitive . Esto es básicamente una capa construida sobre los postulados, por lo que es un poco más agradable. Pero si quieres usar getLine con esto, debes escribir:

import IO.Primitive as Prim

postulate
  primGetLine : Prim.IO Costring

{-# COMPILED primGetLine getLine #-}

getLine : IO Costring
getLine = lift primGetLine

Y finalmente, podemos escribir la función main :

main = run (♯ getLine >>= λ c → ♯ putStrLn⊥ (reverse c))

Al compilar este programa usando Cc Cx Cc y luego ejecutarlo, obtenemos lo esperado:

$ cat test
hello world
$ prog < test    
dlrow olleh

Answer 2

Saizan en #agda señala que uno podría postular que getLine : IO String lugar de getLine : IO Costring . Esto funciona. Entonces obtienes:

module EchoInputReverse where

-- Agda standard library 0.7
open import Data.List using (reverse)
open import Data.String
open import Foreign.Haskell using (Unit)
open import IO.Primitive

postulate
  getLine : IO String

{-# COMPILED getLine getLine #-}

main : IO Unit
main = 
  getLine >>= (λ s → 
  return (toCostring (fromList (reverse (toList s)))) >>= (λ s'' → 
  putStrLn s''))

La desventaja es que este enfoque afirma que getLine siempre devuelve una cadena finita , lo que puede no ser correcto en el caso de prog < /dev/zero como señala @Vitus.

Pero no creo que esto importe. Si getLine de hecho devuelve una cadena infinita, entonces ni esta solución ni la solución de getLine arrojarán un programa que finaliza. Ellos tienen un comportamiento equivalente.

Sería ideal detectar si la entrada era infinita y producir un error en ese caso. Pero este tipo de detección de infinito en IO no es posible en general.