home.social

#agda2hs — Public Fediverse posts

Live and recent posts from across the Fediverse tagged #agda2hs, aggregated by home.social.

fetched live
  1. Jesper Agdakx 🔸 @[email protected] ·

    I’m working on adding some support for Haskell exceptions to agda2hs. I needed to do something so make throw not break soundness so I added an (erased instance) argument of some postulated type MayThrow exc, essentially making all exceptions be checked exceptions on the Agda side.

    I know there’s much nicer ways to exceptions in dependent type theory (i.e. exceptional type theory by PMP et al) but given that Agda doesn’t implement that, this seems like a decent first step. I’m curious to hear any comments you have!

    https://github.com/agda/agda2hs/pull/445

    #Agda #Haskell #Agda2Hs #Exceptions

    #agda #agda2hs #exceptions #haskell
  2. Jesper Agdakx 🔸 @[email protected] ·

    I’m working on adding some support for Haskell exceptions to agda2hs. I needed to do something so make throw not break soundness so I added an (erased instance) argument of some postulated type MayThrow exc, essentially making all exceptions be checked exceptions on the Agda side.

    I know there’s much nicer ways to exceptions in dependent type theory (i.e. exceptional type theory by PMP et al) but given that Agda doesn’t implement that, this seems like a decent first step. I’m curious to hear any comments you have!

    https://github.com/agda/agda2hs/pull/445

    #Agda #Haskell #Agda2Hs #Exceptions

    #agda #agda2hs #exceptions #haskell
  3. Jesper Agdakx 🔸 @[email protected] ·
    Agda2Hs v1.4 has just been released! Find the list of changes here: hackage.haskell.org/package/agda2hs-1.4/changelog

    Get it from your local Hackage or Github shop.

    #Agda #Agda2Hs #DependentTypes
    #agda #agda2hs #dependenttypes
  4. Jesper Agdakx 🔸 @[email protected] ·
    Agda2Hs v1.4 has just been released! Find the list of changes here: hackage.haskell.org/package/agda2hs-1.4/changelog

    Get it from your local Hackage or Github shop.

    #Agda #Agda2Hs #DependentTypes
    #agda #agda2hs #dependenttypes
  5. Jesper Agdakx 🔸 @[email protected] ·
    I just uploaded a release candidate for agda2hs 1.3 to hackage.haskell.org/package/agda2hs-1.3/candidate. Feel free to take it for a test drive!

    Changes to agda2hs:
    - Increased Agda base version to 2.7
    - Increased bounds to support GHC 9.8.4 and GHC 9.10.2
    - Re-implemented the canonicity check for instances to be simpler but more robust
    - Added {-# COMPILE AGDA2HS ... inline #-} pragma for marking definitions to be inlined during compilation to Haskell
    - Added {-# COMPILE AGDA2HS ... tuple #-} pragma for compiling record types in Agda to a tuple type in Haskell
    - Non-erased implicit arguments and instance arguments are now compiled to regular arguments in Haskell
    - Non-erased module parameters are now compiled to regular arguments in Haskell
    - Rank-N Haskell types are now supported

    Additions to the agda2hs Prelude:
    - New module `Haskell.Extra.Dec` for working with decidability proofs (compiled to `Bool`)
    - New module `Haskell.Extra.Refinement` for working with refinement types (compiled to the base type)
    - New module `Haskell.Extra.Erase` for working with erased types (compiled to `()`)
    - New module `Haskell.Extra.Sigma` for working with dependent pair types (compiled to tuples)
    - New module `Haskell.Extra.Loop` providing a safe `loop` function (using an erased fuel argument)
    - New module `Haskell.Extra.Delay` providing a `Delay` monad for non-termination (compiled to pure functions in Haskell)
    - New function `the` in `Haskell.Prim` for generating Haskell type annotations
    - Added properties to `Haskell.Law.Equality`: `subst`, `subst0`
    - Added properties to `Haskell.Law.Bool`: `ifFlip`, `ifTrueEqThen`, `ifFalseEqThen`
    - Added properties to `Haskell.Law.List`: `map-concatMap`, `map-<*>-recomp`, `concatMap-++-distr`
    - Added proofs that many of the instances defined in the prelude are lawful

    #Agda #haskell #agda2hs
    #agda #agda2hs #haskell
  6. Jesper Agdakx 🔸 @[email protected] ·
    I just uploaded a release candidate for agda2hs 1.3 to hackage.haskell.org/package/agda2hs-1.3/candidate. Feel free to take it for a test drive!

    Changes to agda2hs:
    - Increased Agda base version to 2.7
    - Increased bounds to support GHC 9.8.4 and GHC 9.10.2
    - Re-implemented the canonicity check for instances to be simpler but more robust
    - Added {-# COMPILE AGDA2HS ... inline #-} pragma for marking definitions to be inlined during compilation to Haskell
    - Added {-# COMPILE AGDA2HS ... tuple #-} pragma for compiling record types in Agda to a tuple type in Haskell
    - Non-erased implicit arguments and instance arguments are now compiled to regular arguments in Haskell
    - Non-erased module parameters are now compiled to regular arguments in Haskell
    - Rank-N Haskell types are now supported

    Additions to the agda2hs Prelude:
    - New module `Haskell.Extra.Dec` for working with decidability proofs (compiled to `Bool`)
    - New module `Haskell.Extra.Refinement` for working with refinement types (compiled to the base type)
    - New module `Haskell.Extra.Erase` for working with erased types (compiled to `()`)
    - New module `Haskell.Extra.Sigma` for working with dependent pair types (compiled to tuples)
    - New module `Haskell.Extra.Loop` providing a safe `loop` function (using an erased fuel argument)
    - New module `Haskell.Extra.Delay` providing a `Delay` monad for non-termination (compiled to pure functions in Haskell)
    - New function `the` in `Haskell.Prim` for generating Haskell type annotations
    - Added properties to `Haskell.Law.Equality`: `subst`, `subst0`
    - Added properties to `Haskell.Law.Bool`: `ifFlip`, `ifTrueEqThen`, `ifFalseEqThen`
    - Added properties to `Haskell.Law.List`: `map-concatMap`, `map-<*>-recomp`, `concatMap-++-distr`
    - Added proofs that many of the instances defined in the prelude are lawful

    #Agda #haskell #agda2hs
    #agda #agda2hs #haskell
  7. Jesper Agdakx ♾️ @[email protected] ·

    I'm very happy to announce the release of #agda2hs version 1.1, which adds compatibility with #Agda 2.6.4. You can find it at your favorite local Hackage mirror or at hackage.haskell.org/package/ag.

    #agda2hs #agda
  8. Jesper Agdakx ♾️ @[email protected] ·

    agda2hs v1.0 has officially been released and is now available at hackage.haskell.org/package/ag or on a cabal near you! Find the (WIP) documentation at agda.github.io/agda2hs/ and more details about the rationale in our paper dl.acm.org/doi/10.1145/3546189

    #Agda #Haskell #agda2hs

    #agda #haskell #agda2hs
  9. Jesper Agdakx ♾️ @[email protected] ·

    agda2hs v1.0 has officially been released and is now available at hackage.haskell.org/package/ag or on a cabal near you! Find the (WIP) documentation at agda.github.io/agda2hs/ and more details about the rationale in our paper dl.acm.org/doi/10.1145/3546189

    #Agda #Haskell #agda2hs

    #agda #haskell #agda2hs
  10. Jesper Agdakx ♾️ @[email protected] ·

    Ryan Orendorff recently gave a talk about #agda2hs in the SF Haskell meetup, and you can now watch the recording: youtube.com/watch?v=LCuWkTrbxf

    #agda2hs
  11. Jesper Agdakx ♾️ @[email protected] ·

    Ryan Orendorff recently gave a talk about #agda2hs in the SF Haskell meetup, and you can now watch the recording: youtube.com/watch?v=LCuWkTrbxf

    #agda2hs
  12. Jesper Agdakx ♾️ @[email protected] ·

    Wait there was a meetup talking about #agda2hs and 50 people attended and I didn't even know?! Wow, I should probably get working on the 1.0 release again soon. meetup.com/bay-area-haskell-us

    #agda2hs
  13. Jesper Agdakx ♾️ @[email protected] ·

    I was on the Haskell Interlude podcast with @tritlo and Niki Vazou! Listen to it here: haskell.foundation/podcast/20/

    #Haskell #Agda #agda2hs #podcast

    #haskell #agda #agda2hs #podcast