Wouter Swierstra | 15 Apr 16:01 2014
Picon

Haskell Symposium: Second call for papers

===================================================================
                ACM SIGPLAN
                HASKELL SYMPOSIUM 2014
                SECOND CALL FOR SUBMISSIONS

    Gothenburg, Sweden, 4-5 September 2014, directly after ICFP
    http://www.haskell.org/haskell-symposium/2014
    haskell2014@...
===================================================================

The ACM SIGPLAN Haskell Symposium 2014 will be colocated with the 2014
International Conference on Functional Programming (ICFP) in
Gothenburg, Sweden. Like last year, the symposium will last 2 days.
Thanks to broader participation from a growing community, we will be
able to include more regular papers as well as system demonstrations,
while upholding the scientific quality of the symposium.

The Haskell Symposium seeks to present original research on Haskell,
to discuss practical experience and future development of the
language, as well as to promote other forms of denotative programming.
Topics of interest include

* Language Design, with a focus on possible extensions and
  modifications of Haskell as well as critical discussions of the
  status quo;

* Theory, such as formal semantics of the present language or future
  extensions, type systems, effects, metatheory, and foundations for
  program analysis and transformation;

(Continue reading)

Amal Ahmed | 15 Apr 10:55 2014

Oregon PL Summer School: register by May 2nd

*** The registration deadline for this year's Oregon PL Summer School has been extended to May 2nd.
This year's Oregon Programming Languages Summer School will take place from June 16th to 28th, 2014. Full information on registration and scholarships an be found here: http://www.cs.uoregon.edu/Activities/summerschool The school has a long and successful tradition (sponsored by the NSF, ACM SIGPLAN, and industry). It covers current research in the theory and practice of programming languages. Material is presented at a tutorial level that will help graduate students and researchers from academia or industry understand the critical issues and open problems confronting the field. Prerequisites are an elementary knowledge of logic and mathematics, as covered in undergraduate classes on discrete mathematics, and some knowledge of programming languages at the level of an undergraduate survey course. This year we will again offer a Coq boot camp session, to be held on June 15th -- one day before the summer school officially begins. The boot camp will provide a one-day, intensive, hands-on introduction to the practical mechanics of the Coq proof assistant. The Coq boot camp will be run by Michael Clarkson (George Washington University). More information is available at the above website.
This year's program is titled Types, Logic, Semantics, and Verification.  The speakers and topics include: 

Andrew Appel -- Software Verification
Princeton University

Lars Birkedal -- Category Theory
Aarhus University

Michael Clarkson -- Coq Bootcamp
George Washington University

Derek Dreyer -- Modular Reasoning about Stateful Programs
Max Planck Institute for Software Systems

Robert Harper -- Type Theory Foundations
Carnegie Mellon University

Greg Morrisett -- Certified Programming and State
Harvard University

Ulf Norell -- Programming in Agda
Chalmers University of Technology

Brigitte Pientka -- Proof Theory Foundations
McGill University

Stephanie Weirich -- Designing Dependently-Typed Programming Languages
University of Pennsylvania

Steve Zdancewic -- Software Foundations in Coq
University of Pennsylvania

We hope you can join us for this excellent program!

Amal Ahmed
Zena Ariola
Greg Morrisett
OPLSS 2014 organizers




_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Belikov, Evgenij | 14 Apr 19:24 2014
Picon
Picon

Summer School on Advances in Programming Langauges

 Dear all,

 Find below the call for applications to attend the AiPL'14 Summer School.
 Apologies for multiple postings.

 ===================================================

     2nd International Summer School on Advances in Programming Languages

            19-22 August 2014, Heriot-Watt University, Edinburgh

 The 2nd International Summer School on Advances in Programming Languages
 offers four days of insightful lectures and lab sessions on an engaging
 blend of cutting-edge theoretical and practical techniques delivered by
 international experts. The topics include type systems and dependent types,
 novel programming models, and domain-specific languages, among others.
 The School is primarily intended for postgraduate research students and
 aims to foster international collaboration, and encourages a dialogue
 among early career researchers and renowned scientists.

 Important Dates:
  Application deadline: 30 April 2014
  Notification:         15   May 2014
 
 Speakers:
  Philip Wadler, University of Edinburgh
  Jeremy Gibbons, University of Oxford
  Fritz Henglein, DIKU, University of Copenhagen
  Rita Loogen, Philipps-Universität Marburg
  Hans Vandierendonck, Queen's University Belfast
  Jeremy Singer, University of Glasgow
  Conor McBride, University of Strathclyde
  Michele Weiland, Edinburgh Parallel Computing Centre
  Sven-Bodo Scholz, Heriot-Watt University Edinburgh
  Greg Michaelson, Heriot-Watt University Edinburgh
 
 Cost:
  550 GBP - residential
  350 GBP - no accommodation included

 Futher information is available at:
 http://www.macs.hw.ac.uk/~dsg/events/ISS-AiPL-2014/

 ===================================================

 Evgenij on behalf of the AiPL'14 Organising Committee

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Wouter Swierstra | 14 Apr 10:34 2014
Picon

PhD Position in dependent types, testing & hardware design

==============================================================
VACANCY : 1x Phd position in dependent types, testing & hardware design
==============================================================

The research group of Software Technology is part of the Software
Systems division of in the department of Information and Computer
Science at the Utrecht University. We focus our research on functional
programming, compiler construction, program analysis, validation, and
verification.

Financed by the Netherlands Organisation for Scientific Research
(NWO), we currently have a job opening for:

* 1x PhD researcher (PhD student) Software Technology

The aim of the project is to develop a domain specific language for
testing and verifying hardware, embedded in a general purpose
dependently typed programming language.

Besides research, the successful candidate will be expected to help
supervise MSc students and assist teaching courses.

We aim to start September 1, 2014 at the latest, but preferably
sooner.

---------------------------------
What we are looking for
---------------------------------

The candidate should have an MSc in Computer Science, be highly
motivated, speak and write English well, and be proficient in
producing scientific reports. Knowledge of and experience with at
least one of the following four areas is essential:

 * functional programming, such as Haskell or ML;
 * dependently typed programming, such as Agda, Coq, or Idris;
 * software testing, including familiarity with libraries such as
   QuickCheck and SmallCheck;
 * hardware description languages, such as Lava or VHDL;

---------------------------------
What we offer
---------------------------------

The candidate is offered a full-time position for four years. A
part-time of at least 0.8 fte may also be possible. The salary is
supplemented with a holiday bonus of 8% and an end-of-year bonus of
8,3% per year. In addition we offer: a pension scheme, a partially
paid parental leave, flexible employment conditions. Conditions are
based on the Collective Labour Agreement Dutch Universities. The
research group will provide the candidate with necessary support on
all aspects of the project. More information is available on the
website:

  Terms and employment: http://bit.ly/1elqpM7

A part-time of at least 0.8 fte may also be possible. Salary starts
at EURO 2,083 and increases to EURO 2,664 gross per month in the fourth
year of the appointment.

Utrecht is a great place to live, having been ranked as one of the
happiest places in the world, according to BBC travel.

  Living in Utrecht: http://bitly.com/HdbL0X

---------------------------------
In order to apply
---------------------------------

To apply please attach a letter of motivation, a curriculum vitae, and
(email) addresses of two referees. Make sure to also include a
transcript of the courses you have followed (at bachelor and master
level), with the grades you obtained, and to include a sample of your
scientific writing, such as your master thesis.

It is possible to apply for this position if you are close to
obtaining your Master's. In that case include a letter of your
supervisor with an estimate of your progress, and do not forget to
include at least a sample of your technical writing skills.

Application closes on the May 30th, 2014. You can apply through
the University's website:

  http://ssl1.peoplexs.com/Peoplexs22/CandidatesPortalNoLogin/Vacancy.cfm?PortalID=4124&VacatureID=654004

---------------
Contact
---------------

For further information you can direct your inquiries to:

Wouter Swierstra
phone: +31 (0)30 253 9207
e-mail: w.s.swierstra@...
website: http://www.staff.science.uu.nl/~swier004
Balaji Rao R | 12 Apr 20:26 2014

Agda on GitHub Atom

Hello,

I’m interested to develop an Agda package for the GitHub Atom editor. Can anyone give me pointers on how to
get started on the Agda side ? I would like to start by trying to get highlighting to work.

Any help is appreciated!

Thanks,
Balaji
Amy Felty | 9 Apr 20:40 2014
Picon

LFMTP 2014: 2nd Call for Papers

                            Second Call for Papers
                  LFMTP 2014: 9th International Workshop on
         Logical Frameworks and Meta-languages: Theory and Practice
                               Vienna, Austria
                                July 17, 2014
                     http://complogic.cs.mcgill.ca/lfmtp14/

Affiliated with CSL-LICS 2014 and IJCAR 2014 and held as part of the
Federated Logic Conference (FLoC) and the Vienna Summer of Logic
(VSL), http://vsl2014.at

IMPORTANT DATES
Paper Submission:   May 2
Notification:   June 3
Final papers due:   June 19
Workshop:   July 17

INVITED SPEAKERS:
   Jesper Bengtson (IT University of Copenhagen)
   Edwin Brady (University of St. Andrews)
   Gopalan Nadathur (University of Minnesota)

DESCRIPTION: Logical frameworks and meta-languages form a common
substrate for representing, implementing, and reasoning about a wide
variety of deductive systems of interest in logic and computer
science. Their design and implementation on the one hand and their use
in reasoning tasks ranging from the correctness of software to the
properties of formal computational systems on the other hand have been
the focus of considerable research over the last two decades. This
workshop will bring together designers, implementers, and
practitioners to discuss various aspects impinging on the structure
and utility of logical frameworks, including the treatment of variable
binding, inductive and co-inductive reasoning techniques and the
expressivity and lucidity of the reasoning process.

TOPICS: LFMTP 2014 will provide researchers a forum to present
state-of-the-art techniques and discuss progress in areas such as the
following:
- Encoding and reasoning about the meta-theory of programming
   languages and related formally specified systems.
- Theoretical and practical issues concerning the treatment of
   variable binding, especially the representation of, and reasoning
   about, datatypes defined from binding signatures.
- Logical treatments of inductive and co-inductive definitions and
   associated reasoning techniques.
- New theory contributions: canonical and substructural frameworks,
   contextual frameworks, proof-theoretic foundations supporting binders,
   functional programming over logical frameworks, homotopy type theory.
- Applications of logical frameworks, e.g., in proof-carrying
   architectures such as proof-carrying authorization.
- Techniques for programming with binders in functional programming
   languages such as Haskell, OCaml, or Agda and logic programming
   languages such as lambda Prolog or Alpha-Prolog.
   with encoding programming languages theory will be particularly
   welcome.

SUBMISSIONS: In addition to regular papers, we also solicit "work in
progress" reports, in a broad sense. Those do not need to report
original or fully polished research results, but should be interesting
for the community at large.

Submitted papers should be in PDF, formatted using the ACM SIGPLAN
style guidelines
(http://www.acm.org/sigs/publications/proceedings-templates). The
length is restricted to 8 pages, except for "work in progress" papers,
which are restricted to 4 pages.  Submission is via EasyChair
(https://www.easychair.org/conferences/?conf=lfmtp2014).

Authors of accepted papers are expected to present their paper at the
workshop.

PROCEEDINGS: Accepted regular papers will be included in the
proceedings, which will be published in the ACM International
Conference Proceedings Series, available in the ACM Digital
Library. Authors are encouraged to publish auxiliary material with
their paper (technical appendixes, source code, scripts, test data,
etc.).

PROGRAM COMMITTEE:
   Andreas Abel (Gothenburg University)
   Kaustuv Chaudhuri (Inria)
   Adam Chlipala (MIT)
   Amy Felty, Co-Chair (University of Ottawa)
   Elsa Gunter (University of Illinois, Urbana - Champaign)
   Luigi Liquori (Inria)
   Marino Miculan (University of Udine)
   Brigitte Pientka, Co-Chair (McGill University)
   Jorge Luis Sacchini (CMU Quatar)
   Alwen Tiu (Nanyang Technological University)
Marko van Eekelen | 9 Apr 16:03 2014
Picon

Software Engineering vacancy at Radboud University Nijmegen

Software Engineering vacancy at Radboud University Nijmegen
At the Radboud University we have a vacancy for a full-time assistant professor Software Engineering (tenure track, associate professorship may be considered).
Application deadline May 1, 2014, for full details see http://www.ru.nl/vacatures/details/details_vacature_0?recid=530914.

Responsibilities
- to conduct research in one or more ICIS research areas (see below). ICIS’ main areas of research are Security, Model Based Systems and Intelligent Systems. The professorial staff at ICIS includes Bart Jacobs, Frits Vaandrager, Peter Lucas, Tom Heskes and Herman Geuvers.
- teaching activities will be in the area of software engineering. A number of courses in software engineering are constructed around a student run ‘company’, GipHouse, which produces real software products for real clients under the supervision of Marko van Eekelen. You will also be expected to supervise BSc, MSc and PhD theses. Some contribution to our extensive outreach programme towards school children and the general public would be appreciated. Administrative duties will include local and/or national committee memberships.

Work environment
The ICIS institute received an excellent rating in the latest national research evaluation exercise for computer science (2010). ICIS has educational programmes in both Information Science and Computer Science. In 2014 the Computer Science Bachelor’s and Master’s programmes ranked first, both in the Elsevier Magazine rankings and in the Dutch university information guide KeuzeGids Universiteiten, in which the Computer Science Master’s programme also received the ‘TOP’ classification. Specific educational tracks are Security, Software Science, Data Science, eHealth and Mathematical Foundations.

What we expect from you
- you hold a PhD, and have published international academic publications in the area of software engineering, for example on one of the following topics: Architectural Design, Requirements Engineering, Software Product Quality Improvement, Software Development Methodology, Software Analysis, Software Security, Software Metrics and Software Testing);
- you have several years of postdoctoral experience, preferably gained abroad, and an established international reputation (as evidenced by, for example, conference invitations);
- you have some experience in successfully applying for external funding;
- you have outstanding didactic skills and at least some teaching experience, and a clear vision on teaching;
- you have, or are willing to acquire, an official Dutch university teaching qualification (BKO);
- you are already able to teach in English, and should be able to teach in Dutch within two years;
- you have excellent communication skills towards colleagues, students, and non-mathematicians;
- you are interested in widening your scope in collaborating with researchers from various fields.

Would you like to know more? contact Marko van Eekelen by phoning  +31 24 3653410 or mailing M.vanEekelen-Mttm5w9jbbk@public.gmane.org

Applications
Do you want to be our new colleague? Please apply and include with your application a motivation letter (attn. of Ms. W. van der Pluijm), CV and any required attachments. Applications should include a cover letter, a research statement, a teaching statement, a curriculum vitae, a list of publications, and the names of at least two referees. For more information on the application procedure: +31 24 3652131
Please note: We will only consider applications submitted via our application form (a link can be found in the full text of the vacancy at http://www.ru.nl/vacatures/details/details_vacature_0?recid=530914).

If you know someone who might be interested, please pass this message on.

Kind regards,

Marko van Eekelen, Digital Security, Radboud University Nijmegen
Check out our new  Cyber Security Bachelor programme: http://www.ru.nl/cybersecurity


Kind regards,

Marko van Eekelen
Check out our new  Cyber Security Bachelor programme: http://www.ru.nl/cybersecurity



_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Amal Ahmed | 7 Apr 19:31 2014

Oregon PL Summer School: call for participation

This year's Oregon Programming Languages Summer School will take place from June 16th to 28th, 2014. The registration deadline is April 14th. Full information on registration and scholarships an be found here: http://www.cs.uoregon.edu/Activities/summerschool The school has a long and successful tradition (sponsored by the NSF, ACM SIGPLAN, and industry). It covers current research in the theory and practice of programming languages. Material is presented at a tutorial level that will help graduate students and researchers from academia or industry understand the critical issues and open problems confronting the field. Prerequisites are an elementary knowledge of logic and mathematics, as covered in undergraduate classes on discrete mathematics, and some knowledge of programming languages at the level of an undergraduate survey course. This year we will again offer a Coq boot camp session, to be held on June 15th -- one day before the summer school officially begins. The boot camp will provide a one-day, intensive, hands-on introduction to the practical mechanics of the Coq proof assistant. The Coq boot camp will be run by Michael Clarkson (George Washington University). More information is available at the above website.
This year's program is titled Types, Logic, Semantics, and Verification.  The speakers and topics include: 

Andrew Appel -- Software Verification
Princeton University

Lars Birkedal -- Category Theory
Aarhus University

Derek Dreyer -- Modular Reasoning about Stateful Programs
Max Planck Institute for Software Systems

Robert Harper -- Type Theory Foundations
Carnegie Mellon University

Greg Morrisett -- Certified Programming and State
Harvard University

Ulf Norell -- Programming in Agda
Chalmers University of Technology

Brigitte Pientka -- Proof Theory Foundations
McGill University

Stephanie Weirich -- Designing Dependently-Typed Programming Languages
University of Pennsylvania

Steve Zdancewic -- Software Foundations in Coq
University of Pennsylvania

We hope you can join us for this excellent program!


Amal Ahmed
Zena Ariola
Greg Morrisett
OPLSS 2014 organizers

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Serge Autexier | 7 Apr 09:57 2014
Picon

2nd CfP, VERIFY 2014, 8th Verification Workshop, *Abstract Deadline April 17th, 2014*, Focus Theme: Verification Beyond IT Systems

[Apologies for cross posting]

                        SECOND CALL FOR PAPERS

         8th International Verification Workshop (VERIFY’14)
              in connection with IJCAR 2014 at FLoC 2014
                  July 23–24, 2014, Vienna, Austria

                       http://vsl2014.at/verify

The formal  verification of  critical information  systems has  a long
tradition  as one  of  the  main areas  of  application for  automated
theorem proving. Nevertheless, the area is of still growing importance
as the number of computers  affecting everyday life and the complexity
of  these systems  are  both  increasing. The  purpose  of the  VERIFY
workshop  series is  to  discuss problems  arising  during the  formal
modeling and  verification of  information systems and  to investigate
suitable solutions.  Possible perspectives include those  of automated
theorem proving, tool support, system engineering, and applications.

The VERIFY  workshop series aims  at bringing together people  who are
interested in the development of safety and security critical systems,
in formal  methods, in  the development  of automated  theorem proving
techniques,  and  in  the   development  of  tool  support.  Practical
experiences gained in  realistic verifications are of  interest to the
automated theorem proving community and new theorem proving techniques
should  be transferred  into practice.  The overall  objective of  the
VERIFY workshops is to identify  open problems and to discuss possible
solutions under the theme

What are the verification problems? What are the deduction techniques?

The 2014 edition of VERIFY aims for extending the verification methods
for processes implemented in hard-  and software to processes that may
well include computer-assistance, but have  a large part or a frequent
interaction  with non-computer-based  process  steps.  Hence the  2014
edition will run under the focus theme

                    Verification Beyond IT Systems

A  non-exclusive list of application areas  with these characteristics
are

       * Ambient assisted living
       * Intelligent home systems and processes
       * Business systems and processes
       * Production logistics systems and processes
       * Transportation logistics
       * Clinical processes
       * Social systems and processes (e.g., voting systems)

The scope of VERIFY includes topics such as

       * ATP techniques in verification
       * Case studies (specification & verification)
       * Combination of verification systems
       * Integration of ATPs and CASE-tools
       * Compositional & modular reasoning
       * Experience reports on using formal methods
       * Gaps between problems & techniques
       * Formal methods for fault tolerance
       * Information flow control security
       * Refinement & decomposition
       * Reliability of mobile computing
       * Reuse of specifications & proofs
       * Management of change
       * Safety-critical systems
       * Security models
       * Tool support for formal methods

Submissions are encouraged in one of the following two categories:

A. Regular  paper:  Submissions  in  this  category  should   describe
   previously unpublished  work (completed or in  progress), including
   descriptions of research, tools,  and applications.  Papers must be
   5-14  pages  long (in  EasyChair  style)  or  6-15 pages  long  (in
   Springer LNCS style).

B. Discussion  papers: Submissions  in this  category are  intended to
   initiate discussions and hence should address controversial issues,
   and may include  provocative statements. Papers must  be 3-14 pages
   long  (in EasyChair  style) or  3-15 pages  long (in  Springer LNCS
   style).

Important dates
   Abstract Submission Deadline:    April 17th, 2014
   Paper Submission Deadline:       April 25th, 2014
   Notification of acceptance:      May 20, 2014
   Final version due:               May 27, 2014
   Workshop date:                   July 23–24, 2014

Submission is via EasyChair:
   http://www.easychair.org/conferences/?conf=verify2014

Program Committee

 Serge Autexier (DFKI) - chair
 Bernhard Beckert (Karlsruhe Institute of Technology) - chair
 Wolfgang Ahrendt (Chalmers University of Technology)
 Juan Augusto (Middlesex University)
 Iliano Cervesato (Carnegie Mellon University)
 Jacques Fleuriot (University of Edinburgh)
 Marieke Huisman (University of Twente)
 Dieter Hutter (DFKI GmbH)
 Reiner Hähnle (Technical University of Darmstadt)
 Deepak Kapur (University of New Mexico)
 Gerwin Klein (NICTA and UNSW)
 Joe Leslie-Hurd (Intel Corporation)
 Fabio Martinelli (IIT-CNR)
 Catherine Meadows (NRL)
 Stephan Merz (INRIA Lorraine)
 Tobias Nipkow (TU München)
 Lawrence Paulson (University of Cambridge)
 Johann Schumann (SGT, Inc/NASA Ames)
 Kurt Stenzel (University of Augsburg)
flicky frans | 6 Apr 03:34 2014
Picon

Monads with polymorhic bind.

Hi. I'm trying to implement more or less usable monads with
polymorphic bind. Here is the attempt:

record RawMonad {α β : Level} (M : {γ : Level} → Set γ → Set γ) : Set
(suc (α ⊔ β)) where
  infixl 1 _>>=_
  field
    return : {A : Set α} → A → M A
    _>>=_  : {A : Set α} {B : Set β} → M A → (A → M B) → M B

But β does not mentioned in the type of return, so it produces
unresolved metas from time to time.
It can be used however like this:

open RawMonad {{...}}
module MonoMonad {α} = RawMonad {α} {α}
module MM = MonoMonad {{...}}

test3 : (b : Bool) -> Maybe Set₁
test3 b = boolToMaybe b >>= λ _ -> MM.return Set

But return is always "monomorphic", so it should be just return and
not MM.return. That's how I got this bug:
http://code.google.com/p/agda/issues/detail?id=1094&thanks=1094&ts=1396747124

Some examples: http://lpaste.net/7187804666674020352
Does this approach have another disadvantages? Are there better approaches?
flicky frans | 5 Apr 01:37 2014
Picon

Generic programming and pointfree stuff.

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).
Attachment (lambda.7z): application/x-7z-compressed, 6423 bytes
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda

Gmane