lexi-lambda

Monads and delimited control are very closely related, so it isn’t too hard to understand them in terms of one another. From a monadic point of view, the big idea is that if you have the computation m >>= f, then f is m’s continuation. It’s the function that is called with m’s result to continue execution after m returns.

If you have a long chain of binds, the continuation is just the composition of all of them. So, for example, if you have

m >>= f >>= g >>= h

then the continuation of m is f >=> g >=> h. Likewise, the continuation of m >>= f is g >=> h.

AndrasKovacs

{-# 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

domenkozar

{-# 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

domenkozar

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"

brendanzab

/-
  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
-/

serras

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) = {

robrix

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

sjoerdvisscher

-- 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

mb64

(* 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
*)

brendanzab

(** {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