Skip to content

Instantly share code, notes, and snippets.

Avatar
🤔

Jiří Beneš jiribenes

🤔
View GitHub Profile
@AndrasKovacs
AndrasKovacs / NbESharedQuote.hs
Last active Sep 25, 2022
NbE with implicit sharing in quotation
View NbESharedQuote.hs
{-
At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:
"A simple and efficient implementation of strong call by need by an abstract machine"
https://dl.acm.org/doi/10.1145/3549822
This is right up my alley since I've implemented strong call-by-need evaluation
quite a few times (without ever doing more formal analysis of it) and I'm also
interested in performance improvements. Such evaluation is required in
conversion checking in dependently typed languages.
@brendanzab
brendanzab / record-patching.ml
Last active Sep 13, 2022
Elaboration with Singletons and Record patching
View record-patching.ml
(** {0 Elaboration with Record Patching and Singleton Types}
This is a small implementation of a dependently typed language with
dependent record types, with some additional features intended to make it
more convenient to use records as first-class modules. It was originally
ported from {{: https://gist.github.com/mb64/04315edd1a8b1b2c2e5bd38071ff66b5}
a gist by mb64}.
The type system is implemented in terms of an ‘elaborator’, which type
checks and tanslates a user-friendly surface language into a simpler and
@mb64
mb64 / tychk.ml
Last active Jun 2, 2022
Bidirectional typechecking for higher-rank polymorphism in OCaml, without polymorphic subtyping
View tychk.ml
(* Compile with:
$ ocamlfind ocamlc -package angstrom,stdio -linkpkg tychk.ml -o tychk
Example use:
$ ./tychk <<EOF
> let f = (fun x -> x) : forall a. a -> a
> in f f
> EOF
input : forall a. a -> a
*)
@sjoerdvisscher
sjoerdvisscher / CalcComp.hs
Created Aug 25, 2021
Calculating Dependently-Typed Compilers
View CalcComp.hs
-- https://icfp21.sigplan.org/details/icfp-2021-papers/21/Calculating-Dependently-Typed-Compilers-Functional-Pearl-
{-# LANGUAGE GADTs, DataKinds, TypeOperators, TypeFamilies, TypeApplications, KindSignatures, ScopedTypeVariables #-}
import Control.Applicative
import Data.Kind
import Data.Type.Equality
type family (a :: Bool) || (b :: Bool) :: Bool where
'False || b = b
'True || b = 'True
@robrix
robrix / FoldsAndUnfolds.hs
Created Mar 31, 2021
Recursion schemes over lists, in contrast with foldr/unfoldr
View FoldsAndUnfolds.hs
module FoldsAndUnfolds where
import Data.List -- for unfoldr
class Functor f => Recursive f t | t -> f where
project :: t -> f t
cata :: (f a -> a) -> t -> a
cata alg = go where go = alg . fmap go . project
View program-analysis.md

Program Analysis, a Big Happy Family

The idea behind program analysis is simple, right? You just want to know stuff about your program before it runs, usually because you don't want unexpected problems to arise (those are better in movies.) Then why looking at Wikipedia gives you headaches? Just so many approaches, tools, languages 🤯

In this article I would like to give a glimpse of an overarching approach to program analysis, based on ideas from abstract interpretation. My goal is not to pinpoint a specific technique, but rather show how they have common core concepts, the differences being due mostly to algorithmic challenges. In other words, static analysis have a shared goal, but it's a challenge to make them precise and performant.

Code is meant to be executed by a computer. Take the following very simple function:

fun cantulupe(x) = {
@brendanzab
brendanzab / ArithExprs.lean
Last active Sep 22, 2021
A proof of the correctness of an arithmetic expression compiler and decompiler in Lean 4.
View ArithExprs.lean
/-
A proof of the correctness of an arithmetic expression compiler in Lean 4.
Ported from [expcompile.v], which is part of Derek Dreyer and Gert Smolka's
[course material].
[expcompile.v]: https://www.ps.uni-saarland.de/courses/sem-ws17/expcompile.v
[course material]: https://courses.ps.uni-saarland.de/sem_ws1718/3/Resources
-/
@domenkozar
domenkozar / cachix.org.spec.purs
Created Jan 28, 2021
Automated testing for 404/500 errors
View cachix.org.spec.purs
module Spec where
import Quickstrom
import Data.Foldable (any)
import Data.Maybe (maybe)
import Data.Tuple (Tuple(..))
import Data.String.CodeUnits (contains)
import Data.String.Pattern (Pattern(..))
readyWhen = "body"
@domenkozar
domenkozar / Repl.hs
Last active Feb 25, 2021
Cachix Server Repl using hint
View Repl.hs
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Repl where
import Cachix.Config (readConfig)
import Cachix.Env (setupApp)
import Cachix.Server.Prelude
import qualified Control.Exception.Safe as Safe
import qualified Language.Haskell.Interpreter as Interpreter
import Protolude
@AndrasKovacs
AndrasKovacs / GluedEval.hs
Last active Feb 6, 2022
Non-deterministic normalization-by-evaluation in Olle Fredriksson's flavor.
View GluedEval.hs
{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}
{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:
https://github.com/ollef/sixty
The main idea is that during elaboration, we need different evaluation