[Agda] Generic programming and pointfree stuff.

[flicky frans]

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.

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?

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?

I can describe the algorithm, if someone is curious, but there is
nothing extra — just Hindley-Milner, lifting ℕ to Fin and replacing
abstract types with agda's specific. The only tricky part is dealing
with lambda application. When you have STApp e1 e2, you need to make a
function from e1 and a function from e2 (id, if e2 is variable) and
then "merge" them. It's hard to merge functions like (\x1 x3 -> x3)
(\x2 x4 x5 -> x2 (x5 x4)), so instead of returning id for variables,
reduce function returns (\x1 ... xn -> xi), where "n" is a number of
variables in a whole term and "i" corresponds to the specific
variable. Merging is trivial then: (\x1 ... xn -> f) (\x1 ... xn -> x)
=> (\x1 ... xn -> f x).
-------------- next part --------------
A non-text attachment was scrubbed...
Name: lambda.7z
Type: application/x-7z-compressed
Size: 4754 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20140405/c137db6a/lambda.bin