How to write arity-generic functions in Agda? Is it possible to write fully dependent and universe polymorphic arity-generic functions?
相关问题
- Caugth ClassCastException in my Java application
- Get the result of Func<object> when object i
- Rewriting with John Major's equality
- how to interpret REL in agda
- C++ Why does error “no matching function” appear w
相关文章
- Identifying Differences Efficiently
- Agda: Reading a line of standard input as a String
- Recreating Lisp's `apply` in Haskell using GAD
- Haskell: Specifying equal-length constraints of li
- How to index an “element” type by a “source contai
- Haskell Deriving Mechanism for Agda
- Pattern match on specialised constructors
- Defining non-unary functions in Cubical mode
I'll take an n-ary composition function as an example.
The simplest version
Here is how
N-ary
is defined in theData.Vec.N-ary
module:I.e.
comp
receives a numbern
, a functiong : Y -> Z
and a functionf
, which has the arityn
and the resulting typeY
.In the
comp 0 g y = {!!}
case we havehence the hole can be easily filled by
g y
.In the
comp (suc n) g f = {!!}
case,N-ary (suc n) X Y
reduces toX -> N-ary n X Y
andN-ary (suc n) X Z
reduces toX -> N-ary n X Z
. So we haveC-c C-r reduces the hole to
λ x -> {!!}
, and nowGoal : N-ary n X Z
, which can be filled bycomp n g (f x)
. So the whole definition isI.e.
comp
receivesn
arguments of typeX
, appliesf
to them and then appliesg
to the result.The simplest version with a dependent
g
When
g
has type(y : Y) -> Z y
what should be there in the hole? We can't use
N-ary n X Z
as before, becauseZ
is a function now. IfZ
is a function, we need to apply it to something, that has typeY
. But the only way to get something of typeY
is to applyf
ton
arguments of typeX
. Which is just like ourcomp
but only at the type level:And
comp
then isA version with arguments with different types
There is the "Arity-generic datatype-generic programming" paper, that describes, among other things, how to write arity-generic functions, that receive arguments of different types. The idea is to pass a vector of types as a parameter and fold it pretty much in the style of
N-ary
:However Agda is unable to infer that vector, even if we provide its length. Hence the paper also provides an operator for currying, which makes from a function, that explicitly receives a vector of types, a function, that receives
n
implicit arguments.This approach works, but it doesn't scale to fully universe polymorphic functions. We can avoid all these problems by replacing the
Vec
datatype with the_^_
operator:A ^ n
is isomorphic toVec A n
. Then our newN-ary
isAll types lie in
Set
for simplicity.comp
now isAnd a version with a dependent
g
:Fully dependent and universe polymorphic
comp
The key idea is to represent a vector of types as nested dependent pairs:
The second case reads like "there is a type
X
such that all other types depend on an element ofX
". Our newN-ary
is trivial:An example:
But what are the types of
Z
andg
now?Recall that
f
previously had typeXs ->ⁿ Y
, butY
now is hidden in the end of these nested dependent pairs and can depend on an element of anyX
fromXs
.Z
previously had typeY -> Set γ
, hence now we need to appendSet γ
toXs
, making allx
s implicit:OK,
Z : Xs ⋯>ⁿ Set γ
, what type hasg
? Previously it was(y : Y) -> Z y
. Again we need to append something to nested dependent pairs, sinceY
is again hidden, only in a dependent way now:And finally
A test:
Note the dependency in the arguments and the resulting type of
explicit-replicate
. Besides,Set
lies inSet₁
, whileℕ
andA
lie inSet
— this illustrates universe polymorphism.Remarks
AFAIK, there is no comprehensible theory for implicit arguments, so I don't know, how all this stuff will work, when the second function (i.e.
f
) receives implicit arguments. This test:is passed at least.
comp
can't handle functions, if the universe, where some type lies, depends on a value. For exampleBut it's common for Agda, e.g. you can't apply explicit
id
to itself:The code.