[Agda] Type mismatch? Tipo miskongruas?

[Serge Leblanc]

Dear all, how do indicate that p₀ and p have the same type in this above
example? Apparently, {R = R} is not enough.
Estimata ĉiuj, kiel oni indikas ke p₀ kaj p havas la saman tipon en ĉi
supra ekzemplo ? Ŝajne, {R = R} ne sufiŝas.

  {-# NON_TERMINATING #-}
  parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
  parse′ {R} p₀ = parse″ p₀
    where
      parse″ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
      parse″ {xs = xs} p [] = Colist.fromList xs
      parse″ {R = R}{xs = xs} p (t ∷ s) with t ≐ '\n'
      ... | false = parse″ (∂ p t) (♭ s)
      ... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))

Sinceran dankon pro via venonta helpo.

[Jason -Zhong Sheng- Hu]

just remove all R's from parse″


parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
parse′ {R} p₀ = parse″ p₀
where
parse″ : ∀ {xs} → Parser R xs → Colist Char → Colist R
parse″ {xs = xs} p [] = Colist.fromList xs
parse″ {xs = xs} p (t ∷ s) with t ≐ '\n'
... | false = parse″ (∂ p t) (♭ s)
... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))


Sincerely Yours,

Jason Hu
________________________________
From: Agda <agda-***@lists.chalmers.se> on behalf of Serge Leblanc <***@gmail.com>
Sent: September 13, 2018 11:01:48 AM
To: ***@lists.chalmers.se
Subject: [Agda] Type mismatch? Tipo miskongruas?

Dear all, how do indicate that p₀ and p have the same type in this above example? Apparently, {R = R} is not enough.
Estimata ĉiuj, kiel oni indikas ke p₀ kaj p havas la saman tipon en ĉi supra ekzemplo ? Ŝajne, {R = R} ne sufiŝas.

{-# NON_TERMINATING #-}
parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
parse′ {R} p₀ = parse″ p₀
where
parse″ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
parse″ {xs = xs} p [] = Colist.fromList xs
parse″ {R = R}{xs = xs} p (t ∷ s) with t ≐ '\n'
... | false = parse″ (∂ p t) (♭ s)
... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))

Sinceran dankon pro via venonta helpo.

[Jesper Cockx]

You shouldn't rebind the R again in the type signature of parse″, instead
you can just use the same R from the main parse′ function:

{-# NON_TERMINATING #-}
parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
parse′ {R} p₀ = parse″ p₀
where
parse″ : ∀ {xs} → Parser R xs → Colist Char → Colist R
parse″ {xs = xs} p [] = Colist.fromList xs
parse″ {xs = xs} p (t ∷ s) with t ≐ '\n'
... | false = parse″ (∂ p t) (♭ s)
... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))

-- Jesper

Post by Serge Leblanc
Dear all, how do indicate that p₀ and p have the same type in this above
example? Apparently, {R = R} is not enough.
Estimata ĉiuj, kiel oni indikas ke p₀ kaj p havas la saman tipon en ĉi
supra ekzemplo ? Ŝajne, {R = R} ne sufiŝas.
{-# NON_TERMINATING #-}
parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
parse′ {R} p₀ = parse″ p₀
where
parse″ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
parse″ {xs = xs} p [] = Colist.fromList xs
parse″ {R = R}{xs = xs} p (t ∷ s) with t ≐ '\n'
... | false = parse″ (∂ p t) (♭ s)
... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))
Sinceran dankon pro via venonta helpo.
--
Serge Leblanc
------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Nils Anders Danielsson]

Post by Serge Leblanc
{-# NON_TERMINATING #-}
parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
parse′ {R} p₀ = parse″ p₀
where
parse″ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
parse″ {xs = xs} p [] = Colist.fromList xs
parse″ {R = R}{xs = xs} p (t ∷ s) with t ≐ '\n'
... | false = parse″ (∂ p t) (♭ s)
... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))
main = run $ ♯ getContents >>=IO
λ s → ♯ mapM′ (putStrLn ∘ showExpr) (parse′ term s)

One way to avoid using NON_TERMINATING would be to use
IO.readFiniteFile.