Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
    Tesla Ice Zhang‮
    @ice1000
    Try coinductive records
    formrre
    @formrre

    Is there a good reason why agda rejects:

      mutual
       data Ty : Con -> Set where
        ι  : (Γ : Con) -> Ty Γ
        σ  : (Γ : Con) -> (A : Ty Γ) -> Ty (ext Γ A) -> Ty Γ
       data Con : Set where
        ε : Con
        ext : (Γ : Con) -> Ty Γ -> Con

    but accepts the flipped version?

    formrre
    @formrre
    this becomes more troublesome when trying to use cubical version and make Con a higher inductive type
    adding the following to Con: ε ≡ ext ε (ι ε) gets rejected
    with ι not in scope
    Jonas Höfer
    @JonasHoefer
    Hi, I plan to generate some Agda code using Haskell. I'll need a Haskell representation of the AST for that. Are there any plans to outsource the AST from the compiler as a separate package? If not, would it be alright if I extracted the AST from the compiler as a new package (of course referencing the compiler)?
    Jesper Cockx
    @jespercockx
    @formrre this issue seems relevant: agda/agda#2858
    @JonasHoefer Note that the Agda source code as a whole can be used as a Haskell library, this is used for example when developing a custom backend
    however there is no guarantee that the syntax will stay the same in future versions of Agda
    you are of course allowed to extract the AST and use it in your own package if you want (though you should probably check the license)
    Jonas Höfer
    @JonasHoefer
    Okay. Thank you for your quick answer.
    Jonas Höfer
    @JonasHoefer
    I will try working with the Agda package itself.
    Jonas Höfer
    @JonasHoefer
    Hi, I have a short follow-up question regarding Agda code generation. I started experimenting with the Agda package and noticed that there are multiple AST representations. I'm not sure which one I should use, Concrete (A) or Abstract (C). Considering A, is it possible to generate working and readable Agda code from the desugared Abstract representation using AbstractToConcrete.hs? In case of C, do I have to annotate everything with a Range (which isn't NoRange) to pretty print working code? Which one would you recommend?
    Jonas Höfer
    @JonasHoefer
    (Sorry, I of course meant to write "Concrete (C) or Abstract (A)")
    Jesper Cockx
    @jespercockx
    The concrete syntax contains a lot of additional detail that's only really needed for parsing and pretty-printing, so I'd recommend against using that. Depending on your needs, you should probably use either the Abstract syntax (well-scoped, variables are globally unique names) or Internal syntax (well-typed, variables are de-Bruijn indices).
    Jonas Höfer
    @JonasHoefer
    Thank your for your recommendation. I'll look into the internal and the abstract representation.
    Brayan Escobar
    @bdescob_twitter
    Hi all, I'am a novice, could someone give me a log installation guide for a vagrant box image please?
    I mean the OS distribution and the exact terminal commands.This guide doesn't work for me https://agda.readthedocs.io/en/v2.6.1/getting-started/installation.html#
    Jesper Cockx
    @jespercockx
    Can you tell us what exactly goes wrong when you follow the guide?
    Also, what operating system are you using?
    I'm not sure what's a "vagrant box image", maybe some kind of VM?
    MJG
    @marcinjangrzybowski

    Hi, I was suprised that clauses in the extended lambda like :

    test : ℕ → ℕ
    test =  (λ { (suc _) → 2 ; zero → (3 + 1) })

    are not normalised when test is passed to C-c C-n in agda mode
    is this some artefact in the interaction mode ? or maybe in fact those clauses are not normalised and this is proper form ?

    or maybe this is somme issue of converting internal representation to abstract ? is such conversion is used when command C-c C-n is invoked ?
    MJG
    @marcinjangrzybowski

    I think that folowing example shows that indeed clauses in extended lambda are not normalized

    test : ℕ → ℕ
    test =  (λ { (suc _) → 2 ; zero → (3 + 1) })
    
    test' : ℕ → ℕ
    test' =  (λ { (suc _) → 2 ; zero → 4 })
    
    
    zzz : ℕ → ℕ
    zzz = caseNat (3 + 1) 2 
    
    zzz' : ℕ → ℕ
    zzz' = caseNat 4 2 
    
    test= : testtest'
    test= = {!refl!} -- agda do not want to accept refl here
    
    zzz= : zzz ≡ zzz'
    zzz= = refl

    , is it something that can be modified in Agda? or maybe there are deeper reasons why it must be the case?

    MJG
    @marcinjangrzybowski
    definitional equality of extended lambda is more complicated than I though, because even when test, and test' are defined in the exact same way, refl cannot be accepted...
    test : ℕ → ℕ
    test =  (λ { (suc _) → 2 ; zero → 4 })
    
    test' : ℕ → ℕ
    test' =  (λ { (suc _) → 2 ; zero → 4 })
    
    test= : testtest'
    test= = {!refl!} -- do not work
    ok, this subject is already covered in Agda docs :), https://agda.readthedocs.io/en/v2.6.1/language/lambda-abstraction.html
    but my issue is more about normalization than equality, can I force agda to print test' with normalized causes?
    Jesper Cockx
    @jespercockx
    As noted in the documentations, pattern-matching lambdas are syntactic sugar for new top-level definitions, and Agda never normalizes things inside a definition, so the answer is no.
    You could use reflection to write a macro that prints the normalized form of the lambda. This was quite hard to do correctly until recently, but now the reflection API gives access to the clause telescope you need to normalize the body (see agda/agda#2151).
    MJG
    @marcinjangrzybowski
    @jespercockx thanks!
    Yilin Wei
    @yilinwei
    Hello, I have a question on stackoverflow about inference.
    Jacques Carette
    @JacquesCarette
    As far as I can tell, the last activity on here was in late June - is that right?
    Robert Estelle
    @rwe
    Yes, it looks like it. :-/ It does not appear to be very active. The GitHub issues are, but it would be nice to chat synchronously now and then.
    Jacques Carette
    @JacquesCarette
    I would be fine with that too. But right now, there are 4 places, with all of them being fairly dead! That's not good.
    Tesla Ice Zhang‮
    @ice1000
    What are the other three? Did you mean mailing list and IRC?
    Jesper Cockx
    @jespercockx
    Slack, Discord, Zulip
    Jonas Höfer
    @JonasHoefer
    As someone who just uses Agda, where is the best place to ask general questions/were is the community? I have asked some questions here in the past, but was not sure if this is the right place.
    Jesper Cockx
    @jespercockx
    I'd say currently the mailing list still has the biggest reach. Other than that there's Slack (74 members), Gitter (49 members), Discord (53 members), Zulip (42 users), IRC (? users), as well as Reddit and StackOverflow for asking questions. I'm not really sure what's the right place to go either :/
    Jonas Höfer
    @JonasHoefer
    Okay, thank you (:
    Robert Estelle
    @rwe
    Didn’t realize there was a Slack channel, but it looks like signup is restricted to @chalmers.se and @cse.gu.se emails so maybe isn’t meant for general access?
    Jacques Carette
    @JacquesCarette
    The Slack channel isn't supposed to be closed. There was a generic invite on the AIM web site, AFAIK. It was used a lot for AIM, it's been pretty dead since.
    ret394
    @ret394
    Reddit & stack overflow are not for asking Qs. Just remember once. Or do it for science.
    dk14
    @dk14

    Hi! I'd like to use Agda as a target language in a code generator. Here's short description of my problem:
    I have logic (written in haskell) that allows me to generate business rules in a given target language, which is currently a smart-contract language.
    I'd like to prove certain properties about it, but I'd prefer to avoid rewriting those rules in Agda.
    Instead my goal is to generate Agda code automatically and then build proofs on top of generated code.

    Are there convenient APIs in Agda's compiler backend that allow me to type-safely generate Agda AST and pretty-print it into .agda file? Any examples?

    Kyle Raftogianis
    @knrafto
    Agda's internals are available as a haskell library, so you could generate "Concrete" or "Abstract" syntax and use Agda's pretty-printers. I don't think it would be type-safe though, unless you run the agda typechecker over it after
    FWIW, I tried to do something similar (a Haskell compiler from another language to Agda using the Agda API) but eventually I found it was easier to write my own pretty-printer for the subset of Agda I was using ¯\_(ツ)_/¯
    Jorge Blázquez Saborido
    @jorge-jbs
    Related to the conversation about communication channels, Gitter has just been acquired by Element, the company behind Matrix.
    Henry Story
    @bblfish
    Hi, I am learning Agda from the 2017 lectures by Connor McBride. (coming from Scala, but interested in proofs).

    Sometimes it helps to print out values to better understand a structure.

    I can use ctrl-c ctrl-n for single values (in Visual Studio Code). But it's a bit tedious. It would be useful to print to the console or build up a data structure that shows all the values. But if I build a tuple (of sequences) it only shows the first value.

    Jesper Cockx
    @jespercockx
    It might help to ask your question over at https://agda.zulipchat.com/. It's currently very active with the Agda meeting going on!
    Jesper Cockx
    @jespercockx
    We've decided to use Zulip as the official chat for Agda from now on, so please join us at https://agda.zulipchat.com/!