Arity-generic programming in Agda -

-

how write arity-generic functions in agda? possible write dependent , universe polymorphic arity-generic functions?

i'll take n-ary composition function example.

the simplest version

open import data.vec.n-ary  comp : ∀ n {α β γ} {x : set α} {y : set β} {z : set γ}      -> (y -> z) -> n-ary n x y -> n-ary n x z comp  0      g y = {!!} comp (suc n) g f = {!!}

here how n-ary defined in data.vec.n-ary module:

n-ary : ∀ {ℓ₁ ℓ₂} (n : ℕ) → set ℓ₁ → set ℓ₂ → set (n-ary-level ℓ₁ ℓ₂ n) n-ary 0    b = b n-ary (suc n) b = → n-ary n b

i.e. comp receives number n, function g : y -> z , function f, has arity n , resulting type y.

in comp 0 g y = {!!} case have

goal : z y    : y g    : y -> z

hence hole can filled g y.

in comp (suc n) g f = {!!} case, n-ary (suc n) x y reduces x -> n-ary n x y , n-ary (suc n) x z reduces x -> n-ary n x z. have

goal : x -> n-ary n x z f    : x -> n-ary n x y g    : y -> z

c-c c-r reduces hole λ x -> {!!}, , goal : n-ary n x z, can filled comp n g (f x). whole definition is

comp : ∀ n {α β γ} {x : set α} {y : set β} {z : set γ}      -> (y -> z) -> n-ary n x y -> n-ary n x z comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x)

i.e. comp receives n arguments of type x, applies f them , applies g result.

the simplest version dependent g

when g has type (y : y) -> z y

comp : ∀ n {α β γ} {x : set α} {y : set β} {z : y -> set γ}      -> ((y : y) -> z y) -> (f : n-ary n x y) -> {!!} comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x)

what should there in hole? can't use n-ary n x z before, because z function now. if z function, need apply something, has type y. way of type y apply f n arguments of type x. our comp @ type level:

comp : ∀ n {α β γ} {x : set α} {y : set β}      -> (y -> set γ) -> n-ary n x y -> set (n-ary-level α γ n) comp  0      z y = z y comp (suc n) z f = ∀ x -> comp n z (f x)

and comp is

comp : ∀ n {α β γ} {x : set α} {y : set β} {z : y -> set γ}      -> ((y : y) -> z y) -> (f : n-ary n x y) -> comp n z f comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x)

a version arguments different types

there "arity-generic datatype-generic programming" paper, describes, among other things, how write arity-generic functions, receive arguments of different types. idea pass vector of types parameter , fold pretty in style of n-ary:

arrty : {n : n} → vec set (suc n) → set arrty {0}     (a :: []) = arrty {suc n} (a :: as) = → arrty

however agda unable infer vector, if provide length. hence paper provides operator currying, makes function, explicitly receives vector of types, function, receives n implicit arguments.

this approach works, doesn't scale universe polymorphic functions. can avoid these problems replacing vec datatype _^_ operator: 

_^_ : ∀ {α} -> set α -> ℕ -> set α ^ 0     = lift ⊤ ^ suc n = × ^ n

a ^ n isomorphic vec n. our new n-ary is

_->ⁿ_ : ∀ {n} -> set ^ n -> set -> set _->ⁿ_ {0}      _      b = b _->ⁿ_ {suc _} (a , r) b = -> r ->ⁿ b

all types lie in set simplicity. comp is

comp : ∀ n {xs : set ^ n} {y z : set}      -> (y -> z) -> (xs ->ⁿ y) -> xs ->ⁿ z comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x)

and version dependent g:

comp : ∀ n {xs : set ^ n} {y : set}      -> (y -> set) -> (xs ->ⁿ y) -> set comp  0      z y = z y comp (suc n) z f = ∀ x -> comp n z (f x)  comp : ∀ n {xs : set ^ n} {y : set} {z : y -> set}      -> ((y : y) -> z y) -> (f : xs ->ⁿ y) -> comp n z f comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x)

fully dependent , universe polymorphic comp

the key idea represent vector of types nested dependent pairs:

sets : ∀ {n} -> (αs : level ^ n) -> ∀ β -> set (mono-^ (map lsuc) αs ⊔ⁿ lsuc β) sets {0}      _       β = set β sets {suc _} (α , αs) β = Σ (set α) λ x -> x -> sets αs β

the second case reads "there type x such other types depend on element of x". our new n-ary trivial:

fold : ∀ {n} {αs : level ^ n} {β} -> sets αs β -> set (αs ⊔ⁿ β) fold {0}      y      = y fold {suc _} (x , f) = (x : x) -> fold (f x)

an example:

postulate   explicit-replicate : (a : set) -> (n : ℕ) -> -> vec n  test : fold (set , λ -> ℕ , λ n -> , λ _ -> vec n)  test = explicit-replicate

but types of z , g now?

comp : ∀ n {β γ} {αs : level ^ n} {xs : sets αs β} {z : {!!}}      -> {!!} -> (f : fold xs) -> comp n z f comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x)

recall f had type xs ->ⁿ y, y hidden in end of these nested dependent pairs , can depend on element of x xs. z had type y -> set γ, hence need append set γ xs, making xs implicit:

_⋯>ⁿ_ : ∀ {n} {αs : level ^ n} {β γ}       -> sets αs β -> set γ -> set (αs ⊔ⁿ β ⊔ γ) _⋯>ⁿ_ {0}      y      z = y -> z _⋯>ⁿ_ {suc _} (_ , f) z = ∀ {x} -> f x ⋯>ⁿ z

ok, z : xs ⋯>ⁿ set γ, type has g? (y : y) -> z y. again need append nested dependent pairs, since y again hidden, in dependent way now:

Πⁿ : ∀ {n} {αs : level ^ n} {β γ}    -> (xs : sets αs β) -> (xs ⋯>ⁿ set γ) -> set (αs ⊔ⁿ β ⊔ γ) Πⁿ {0}      y      z = (y : y) -> z y Πⁿ {suc _} (_ , f) z = ∀ {x} -> Πⁿ (f x) z

and finally

comp : ∀ n {αs : level ^ n} {β γ} {xs : sets αs β}      -> (xs ⋯>ⁿ set γ) -> fold xs -> set (αs ⊔ⁿ γ) comp  0      z y = z y comp (suc n) z f = ∀ x -> comp n z (f x)  comp : ∀ n {β γ} {αs : level ^ n} {xs : sets αs β} {z : xs ⋯>ⁿ set γ}      -> Πⁿ xs z -> (f : fold xs) -> comp n z f comp  0      g y = g y comp (suc n) g f = λ x -> comp n g (f x)

a test:

length : ∀ {α} {a : set α} {n} -> vec n -> ℕ length {n = n} _ = n  explicit-replicate : (a : set) -> (n : ℕ) -> -> vec n explicit-replicate _ _ x = replicate x  foo : (a : set) -> ℕ -> -> ℕ foo = comp 3 length explicit-replicate  test : foo bool 5 true ≡ 5 test = refl

note dependency in arguments , resulting type of explicit-replicate. besides, set lies in set₁, while ℕ , a lie in set — illustrates universe polymorphism.

remarks

afaik, there no comprehensible theory implicit arguments, don't know, how stuff work, when second function (i.e. f) receives implicit arguments. test:

foo' : ∀ {α} {a : set α} -> ℕ -> -> ℕ foo' = comp 2 length (λ n -> replicate {n = n})  test' : foo' 5 true ≡ 5 test' = refl

is passed @ least.

comp can't handle functions, if universe, type lies, depends on value. example

explicit-replicate' : ∀ α -> (a : set α) -> (n : ℕ) -> -> vec n explicit-replicate' _ _ _ x = replicate x  ... because result in invalid use of setω ... error : ∀ α -> (a : set α) -> ℕ -> -> ℕ error = comp 4 length explicit-replicate'

but it's common agda, e.g. can't apply explicit id itself:

idₑ : ∀ α -> (a : set α) -> -> idₑ _ _ x = x  -- ... because result in invalid use of setω ... error = idₑ _ _ idₑ

the code.


Comments

Post a Comment

Popular posts from this blog

node.js - How to mock a third-party api calls in the backend -

-
i'm testing application mocha , supertest, test like var request = require('supertest'), app = require('./bootstrap.js'); describe('...', function() { it('...', function() { request(app) .get('/some/url') // ... }); }); the bootstrap.js real application before listen ports all works perfect have add calls third-party api , testing slow so when do, test example takes 5 seconds request(app) .get('/my/endpoint/that/makes/call/others') // ... how can make fake calls during test real when running application? you can use nock purpose.
Read more

node.js - Why do I get "SOCKS connection failed. Connection not allowed by ruleset" for some .onion sites? -

-
i'm experimenting node , socks5-https-client . reason, tor hidden service ( .onion ) sites return connection error. for example, connecting duckduckgo ( 3g2upl4pq6kufc4m.onion ) works , returns html. however, connecting pirate bay ( uj3wazyk5u4hnvtk.onion ) or torch ( xmh57jrzrnw6insl.onion ) returns... error: socks connection failed. connection not allowed ruleset. what error mean? how can avoid it? here's code reproduce it: var shttps = require('socks5-https-client'); shttps.get({ hostname: '3g2upl4pq6kufc4m.onion', path: '', sockshost: '127.0.0.1', socksport: 9150, rejectunauthorized: false }, function(res) { res.setencoding('utf8'); res.on('readable', function() { console.log(res.read()); // log response console. }); }); the error seems caused 0x02 value in field 2 of server response. in summary the servers you're failing access don't support ...
Read more

java - Cannot resolve constructor when using ArrayAdapter -

-
i'm getting myself in muddle arrayadapter i'm trying put together. i've got constructor, person, used put people go in list. i'm putting arraylist of type person make readable list. i put arrayadapter list can seen in listview, i'm getting "cannot resolve constructor" code. i've tried countless possible solutions on site including trying use getactivity() or in place of peopleactivity.this, cannot code compile. i've tried referencing constructor class in arrayadapter, gives me error it's not enclosing class. person.class (constructor) import android.text.editable; public class person { public person person; private editable personname; public person(editable a) { personname = a; } public void setname(editable personname){ this.personname = personname; } public editable getname() { return personname; } } peopleactivity - populatelistview arraylist<person> peoplelistv = new arraylist<person>(); ... ...
Read more