wasabi
@wasabi315.bsky.social
:: (PhD Student at ScienceTokyo, traP, Haskell, Agda, OCaml) https://wasabi315.github.io/en/
Are there some theoretical things lurking behind this combinator? I found myself wanting this combinator while running `Fold` in stages. Each stage (generated from `b`) can feed many `a`s into a downstream `Fold` without materialising `[a]`.
I scored 12 / 12 on "Extension Or Imitation" doscienceto.it/extension-or... Try it out? via @doscienceto.it #Haskell #HaskellLanguageExtensionOrImitation
Extension or Imitation?
Can you tell the real Haskell Language Extensions from the Imitations?
doscienceto.it
Wrote a post on a verified pattern-matching coverage checker! wasabi315.github.io/en/posts/ver... (英語版も見れるようにしました！ChatGPT様様...)
A Verified Coverage Checker
Formalizing a pattern-matching coverage-checking algorithm in Agda
wasabi315.github.io
パターンマッチのカバレッジ検査の verified implementationをAgdaでした話をブログに書きました！ wasabi315.github.io/ja/posts/ver...
検証付きカバレッジ検査器
パターンマッチのCoverage CheckingアルゴリズムをAgdaで形式化した
wasabi315.github.io
Published!! dl.acm.org/doi/10.1145/...
Unification Modulo Isomorphisms between Dependent Types for Type-Based Library Search | Proceedings of the 10th ACM SIGPLAN International Workshop on Type-Driven Development
dl.acm.org
wasabi@wasabi315.bsky.social · 11mo agoExcited to present at TyDe2025 in Singapore this October! "Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search" conf.researchr.org/details/icfp...
Excited to present at TyDe2025 in Singapore this October! "Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search" conf.researchr.org/details/icfp...
Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search (TyDe 2025) - ICFP/SPLASH 2025
The Workshop on Type-Driven Development (TyDe) aims to show how static type information may be used effectively in the development of computer programs. Co-located with ICFP, this workshop brings toge...
conf.researchr.org
Made compatible with agda2hs now so it compiles to readable Haskell!! github.com/wasabi315/co...
GitHub - wasabi315/coverage-checking
Contribute to wasabi315/coverage-checking development by creating an account on GitHub.
github.com
wasabi@wasabi315.bsky.social · 2y ago“Warnings for pattern matching”で提案されている網羅性アルゴリズムの一つをAgdaで形式化してる 停止性を除いて正当性を証明できた github.com/wasabi315/ex...
NbE for untyped lambda terms co-De Bruijn indices (in Haskell/Agda)! Seems working! github.com/wasabi315/ki... github.com/wasabi315/ki...
kitchen-sink/haskell/co-debruijn/app/Main.hs at main · wasabi315/kitchen-sink
Contribute to wasabi315/kitchen-sink development by creating an account on GitHub.
github.com
Added a search algorithm in which you can include variables to be unified in the query! github.com/wasabi315/ty...
wasabi@wasabi315.bsky.social · last yr.Creating a collection of type-based library search algorithms🔍 It contains 3 algorithms with different search flexibility currently. github.com/wasabi315/ty...
Creating a collection of type-based library search algorithms🔍 It contains 3 algorithms with different search flexibility currently. github.com/wasabi315/ty...
GitHub - wasabi315/type-search-zoo: A collection of type-based library search algorithms
A collection of type-based library search algorithms - wasabi315/type-search-zoo
github.com
“Warnings for pattern matching”で提案されている網羅性アルゴリズムの一つをAgdaで形式化してる 停止性を除いて正当性を証明できた github.com/wasabi315/ex...
GitHub - wasabi315/exhaustiveness-checking-agda
Contribute to wasabi315/exhaustiveness-checking-agda development by creating an account on GitHub.
github.com
TypeScriptの秘孔を突いてしまった github.com/microsoft/Ty...
`getTypeListId` crashes with `TypeError: Cannot read properties of undefined (reading 'id')` · Issue #59062 · microsoft/TypeScript
🔎 Search Terms getTypeListId, circular reference, conditional types 🕗 Version & Regression Information This is a crash This changed between versions (confirmed using the Playground) ~3.6.3: does no...
github.com
