[Agda] Generic programming and pointfree stuff.

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 05.04.2014 01:37, flicky frans wrote:
> Hi. I'm playing with generic programming in Agda. I've written a 
> function, which can be used to construct combinators. Here are the
> examples: http://lpaste.net/4817148711178076160 Here is the main
> module: http://lpaste.net/1337448319143641088 The whole code is
> attached. I have some questions:
> 
> Why doesn't agda have non-dependent pattern-matching? It's very
> usefull.
> 
> It would be nice to have the opportunity to rename fields in a 
> datatypes. Something like: LTerm  n = TreeLike (Fin n) renaming
> (Leaf to Var; Branch to App) Or just Leaf = Var and Branch = App,
> but with opportunity to use Var and App in the pattern-matching.

You can use the pattern synonym facility:

pattern App = Branch
pattern Var = Leaf

> It takes a time to typecheck the examples, due to a memory leak 
> probably, but I can't figure out, where it happens. Is there
> something like seq or bang patterns in agda?

No, but you could try the development version of Agda (get from the
darcs repo) which has some performance improvements.  (Might be worth
trying.)

> There are a lot of redundant evaluations in the definition of λℕ':
> 
> _>>=T_ : {α : Level} {A : Set α} {k : A -> Level} -> (mx : Maybe A)
> -> ((x : A) -> Set (k x)) -> Set (maybe′ k lzero mx) nothing >>=T f
> = ⊤ just x  >>=T f = f x
> 
> _>>=⊤_ : {α : Level} {A : Set α} {k : A -> Level} {B : (x : A) ->
> Set (k x)} -> (mx : Maybe A) -> ((x : A) -> B x) -> mx >>=T B 
> nothing >>=⊤ _ = _ just x  >>=⊤ f = f x
> 
> λℕ' : {α : Level} -> (n : ℕ) -> (t : LType) -> finifyTreeLikeWith n
> t   >>=T λ term  -> varTypesVec term         >>=T λ types -> 
> finifyTreeLikeVec types  >>=T λ LXs   -> getType LXs term
> >>=T λ type  -> castWithAs LXs type term >>=T λ tterm -> ∀⇒ (λ (Xs
> : Vec (Set α) _) -> vnary (V.map (getSet Xs) LXs) (getSet Xs
> type)) λℕ' n t = finifyTreeLikeWith n t   >>=⊤ λ term  -> 
> varTypesVec term         >>=⊤ λ types -> finifyTreeLikeVec types
> >>=⊤ λ LXs   -> getType LXs term         >>=⊤ λ type  -> castWithAs
> LXs type term >>=⊤ λ tterm -> λ {x} -> λ⇒ (λ Xs -> reduce
> (typifySet (x ∷ Xs) tterm))
> 
> and I don't know, how to fold them. Am I missing something or it's
> a nontrivial thing?
> 
> It should be
> 
> λ⇒ (λ Xs -> reduce (typifySet Xs tterm))
> 
> instead of
> 
> λ {x} -> λ⇒ (λ Xs -> reduce (typifySet (x ∷ Xs) tterm))
> 
> due to the fact, that Xs is always X ∷ Xs' for some X and Xs', and
> the definition of λ⇒, which I've stolen from the Arity-Generic 
> Datatype-Generic Programming paper:
> 
> ∀⇒ : {l : ℕ} {α β : Level} {A : Set α} -> (Vec A l -> Set β) -> Set
> (naryLevel l α β) ∀⇒ {0}     B = B [] ∀⇒ {suc l} B = ∀ {x} -> ∀⇒ (λ
> xs -> B (x ∷ xs))
> 
> λ⇒ : {l : ℕ} {α β : Level} {A : Set α} {B : Vec A l -> Set β} ->
> ((xs : Vec A l) -> B xs) -> ∀⇒ B λ⇒ {0}     f = f [] λ⇒ {suc l} f =
> λ {x} -> λ⇒ (λ xs -> f (x ∷ xs))
> 
> And agda agrees with me, when it refines a hole, but complains,
> when typechecks the whole module. Here is the error:
> 
> Set (L.foldr _⊔_ (L.foldr _⊔_ (_α_570 n t x x₁ x₂ x₃ x₄) 
> (L.replicate n (_α_570 n t x x₁ x₂ x₃ x₄))) (L.replicate (V.foldr
> (λ _ → ℕ) (λ {.n} x → N._⊔_ (maxNatTreeLike x)) 0 x₁) (lsuc (_α_570
> n t x x₁ x₂ x₃ x₄)))) != Set (lsuc .α ⊔ L.foldr _⊔_ (L.foldr _⊔_ .α
> (L.replicate n .α)) (L.replicate (V.foldr (λ _ → ℕ) (λ {.n} x →
> N._⊔_ (maxNatTreeLike x)) 0 x₁) (lsuc .α))) when checking that the
> expression ... has type...
> 
> So agda looses the "lsuc .α ⊔" part. I tried to explicitly
> instantiate as much, as possible, but agda only gives more precise
> errors like Set ... != Set (lsuc α ⊔ ...). What's going wrong?

Conversion checking for Level is certainly incomplete.  Levels are not
meant for complicated computations.

You could file a bug report (google for "agda issues") with a file
that reproduces the problematic behavior.



- -- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iEYEARECAAYFAlM/7R0ACgkQPMHaDxpUpLPGZgCg4OTvdP4Tgl0ddQNGNzwvAB5P
AxAAoIl4f9n4wl3FACybVHDWgZKmk3nZ
=3lua
-----END PGP SIGNATURE-----