Gavinok

;; eglot-codelens.el --- Add support for codelenses to eglot -*- lexical-binding: t -*-
;;; Commentary:
;;; Code:
;;; Extending eglot to support lenses

;;;; Findings
;; Lenses often support the option to be used as a code action
;; some servers rely on custom code actions implemented by the client
;; - [[https://github.com/emacs-lsp/lsp-mode/issues/2250]] mentions this

emekoi

#!/usr/bin/sh

set -e

files="$(fd -e .el .)"

sd -s '^\\\\\\\\begin{code}' '^[\t ]*\```\s*haskell.*?' $files
sd -s '\\\\begin{code}' '```\s*haskell.*?' $files
sd -s '\\begin{code}' '```\s*haskell.*?' $files
sd -s '^\\\\\\\\end{code}' '^[\t ]*\```' $files

VictorTaelin

Implementing complex numbers and FFT with just datatypes (no floats)

In this article, I'll explain why implementing numbers with just algebraic datatypes is desirable. I'll then talk about common implementations of FFT (Fast Fourier Transform) and why they hide inherent inefficiencies. I'll then show how to implement integers and complex numbers with just algebraic datatypes, in a way that is extremely simple and elegant. I'll conclude by deriving a pure functional implementation of complex FFT with just datatypes, no floats.

hirrolot

This is a minimalistic OCaml implementation of the type system from chapter 30 of TAPL, "Higher-Order Polymorphism".

The implementation uses bidirectional typing and does not feature existential types. Binders are represented as metalanguage functions (HOAS-style); free variables (TyFreeVar & FreeVar) are represented as De Bruijn levels.

See also:

• "Barebones lambda cube in OCaml"
• "How to implement dependent types in 80 lines of code"

hirrolot

type cps_var =
  (* Taken from the lambda term during CPS conversion. *)
  | CLamVar of string
  (* Generated uniquely during CPS conversion. *)
  | CGenVar of int

type cps_term =
  | CFix of (cps_var * cps_var list * cps_term) list * cps_term
  | CAppl of cps_var * cps_var list
  | CRecord of cps_var list * binder

AndrasKovacs

{-# language BlockArguments, LambdaCase, Strict, UnicodeSyntax #-}

{-|
Minimal dependent lambda caluclus with:
  - HOAS-only representation
  - Lossless printing
  - Bidirectional checking
  - Efficient evaluation & conversion checking

Inspired by https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196

hirrolot

type term =
  | Lam of (term -> term)
  | Pi of term * (term -> term)
  | Appl of term * term
  | Ann of term * term
  | FreeVar of int
  | Star
  | Box

let unfurl lvl f = f (FreeVar lvl)

gelisam

-- Defining a custom recursion scheme to manipulate two mutually-recursive
-- types, in the context of a toy bidirectional type checker.
{-# LANGUAGE DerivingStrategies, GeneralizedNewtypeDeriving, ScopedTypeVariables #-}
module Main where

import Test.DocTest

import Control.Monad (when)
import Data.Bifunctor (Bifunctor(bimap))
import Data.Bifoldable (Bifoldable(bifoldMap), bitraverse_)

AndrasKovacs

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

karthick18

/*
 * An example using vmsplice to move user space buffers to pipe before using 
 * splice syscall which avoids copying to/from user space buffers to kernel space
 * and uses the pipe buffers allocated in kernel space as an intermediate to directly xfer from one file to another
 *
 * gcc -o splice splice.c -g
 */

#define _GNU_SOURCE
#include <stdio.h>