VictorTaelin

// A nano dependent type-checker featuring inductive types via self encodings.
// All computation rules are justified by interaction combinator semantics,
// resulting in major simplifications and improvements over old Kind-Core.
// Specifically, computable annotations (ANNs) and their counterpart (ANN
// binders) and a new self encoding based on equality (rather than dependent
// motives) greatly reduce code size. A more complete file, including
// superpositions (for optimal unification) is available on the
// Interaction-Type-Theory repository.
// Credits also to Franchu and T6 for insights.

AndrasKovacs

Garbage collection with zero cost at non-GC time

Every once in a while I investigate low-level backend options for PL-s, although so far I haven't actually written any such backend for my projects. Recently I've been looking at precise garbage collection in popular backends, and I've been (like on previous occasions) annoyed by limitations and compromises.

I was compelled to think about a system which accommodates precise relocating GC as much as possible. In one extreme configuration, described in this note, there

mndrix

type t = Lexing.lexbuf -> Parser.token

val of_file : string -> t * Lexing.lexbuf
(** [of_file path] returns a new lexer for extracting tokens from
a file at [path]. *)

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)

tfausak

-- https://downloads.haskell.org/~ghc/9.0.1/docs/html/users_guide/extending_ghc.html#compiler-plugins
-- https://downloads.haskell.org/~ghc/9.0.1/docs/html/libraries/ghc-9.0.1/GHC-Plugins.html

module DerivingViaPlugin where

import qualified Control.Monad as Monad
import qualified GHC.Data.Bag as G
import qualified GHC.Hs as G
import qualified GHC.Plugins as P
import qualified GHC.Types.Basic as G

emilypi

;;; Code:
(global-set-key (kbd "M-g a") "α")
(global-set-key (kbd "M-g b") "β")
(global-set-key (kbd "M-g g") "γ")
(global-set-key (kbd "M-g d") "δ")
(global-set-key (kbd "M-g e") "ε")
(global-set-key (kbd "M-g z") "ζ")
(global-set-key (kbd "M-g h") "η")
(global-set-key (kbd "M-g q") "θ")
(global-set-key (kbd "M-g i") "ι")

ekmett

{- cabal:
build-depends: base, constraints
-}
{-# language TypeFamilies, TypeFamilyDependencies, ConstraintKinds, ScopedTypeVariables, NoStarIsType, TypeOperators, TypeApplications, GADTs, AllowAmbiguousTypes, FunctionalDependencies, UndecidableSuperClasses, UndecidableInstances, FlexibleInstances, QuantifiedConstraints, BlockArguments, RankNTypes, FlexibleContexts, StandaloneKindSignatures, DefaultSignatures  #-}

 -- ⊷, ≕, =∘, =◯ These choices all look like something out of Star Trek, so let's boldly go...

import Data.Constraint hiding (top, bottom, Bottom)
import Data.Kind
import Data.Some

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

xgrommx

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module TLRecursionSchemes where

import qualified GHC.TypeLits as TL

inamiy

-- Solving Fix / Mu / Nu exercise in
-- https://stackoverflow.com/questions/45580858/what-is-the-difference-between-fix-mu-and-nu-in-ed-kmetts-recursion-scheme-pac

{-# LANGUAGE RankNTypes, GADTs #-}

----------------------------------------
-- Fix / Mu / Nu

newtype Fix f = Fix { unFix :: f (Fix f) }