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

neel-krishnaswami

module C : sig
  type t 
  val empty : t 
  val one : char -> t 
  val union : t -> t -> t 
  val inter : t -> t -> t 
  val top : t 
  val mem : char -> t -> bool 
  val make : (char -> bool) -> t 
  val equal : t -> t -> bool

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.

luc-tielen

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Bad where

import Prelude
import Data.Kind ( Type )
import Generics.MultiRec.TH

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

paf31

## Principal type-schemes for functional programs

**Luis Damas and Robin Milner, POPL '82**

> module W where

> import Data.List
> import Data.Maybe
> import Data.Function

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

depp

// Faster solution for:
// http://www.boyter.org/2017/03/golang-solution-faster-equivalent-java-solution/
// With threading.
// g++ -std=c++11 -Wall -Wextra -O3 -pthread

// On my computer (i5-6600K 3.50 GHz 4 cores), takes about ~160 ms after the CPU
// has warmed up, or ~80 ms if the CPU is cold (due to Turbo Boost).

// How it works: Start by generating a list of losing states -- states where the
// game can end in one turn.  Generate a new list of states by running the game

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

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