rntz

(* Inlining for the λ-calculus, implemented in tagless final style. This seems
 * like it _must_ be related to Normalization By Evaluation (see eg [1,2]),
 * since they both amount to β-reduction (plus η-expansion in extensional NBE),
 * and the techniques have a similar "flavor", but I don't immediately see a
 * formal connection.
 *
 * [1] https://gist.github.com/rntz/f2f15f6cb4b8690c3599119225a57d33
 * [2] http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
 *)

wilbowma

\documentclass{article}

\usepackage{mathpartir}
\usepackage{tikz}

% Play with xshift and yshift if it looks funny
\newcommand{\tikzmark}[1]{\tikz[overlay,remember picture,xshift=-3pt,yshift=1pt] \node (#1) {};}

\begin{document}
\[

proger

pi = nn.Parameter(torch.randn(len(zk), len(zk)))
# enforce the constraint that we never transfer
# to the start tag and we never transfer from the stop tag
pi.data[0, :] = -10000
pi.data[:, len(zk)-1] = -10000
pi

# pi[to, :] == pi[to]
# pi[:, from_]

xuanruiqi

%default total

data Tree : (a : Type) -> Nat -> Type where
     Leaf : Ord a => Tree a 0
     Node2 : {h : Nat} -> Tree a h -> a -> Tree a h -> Tree a (S h)
     Node3 : {h : Nat} -> Tree a h -> a -> Tree a h -> a -> 
                         Tree a h -> Tree a (S h)
                               
height : Tree a n -> Nat
height Leaf = 0

RyanGlScott

I've discovered something how to do something that GHC never intended you to be able to do, and I'm wondering if there's a way to abuse this to do interesting things.

It's known that you can express visible, dependent quantification at the kind level:

data A a :: a -> Type

λ> :kind A

i-am-tom

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}

rntz

(* Based on http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf *)
exception TypeError

type tp = Base | Fn of tp * tp
let subtype (x: tp) (y: tp): bool = x = y

type sym = {name: string; id: int}

let next_id = ref 0
let nextId() = let x = !next_id in next_id := x + 1; x

UlfNorell

-- Reversing an ascending list in Agda.
-- Challenge by @arntzenius: https://twitter.com/arntzenius/status/1034919539467677696
module AscList where

-- We'll go without libraries to make things clearer.

flip : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (A → B → C) → B → A → C
flip f x y = f y x

-- Step one is to define ordered lists. We'll roughly follow Conor McBride's approach

fay59

Here's a list of mildly interesting things about the C language that I learned mostly by consuming Clang's ASTs. Although surprises are getting sparser, I might continue to update this document over time.

There are many more mildly interesting features of C++, but the language is literally known for being weird, whereas C is usually considered smaller and simpler, so this is (almost) only about C.

1. Combined type and variable/field declaration, inside a struct scope [https://godbolt.org/g/Rh94Go]

struct foo {
   struct bar {
 int x;

taktoa

A Self-Taught Course in Automated Reasoning using Haskell

Variables, Terms, and Syntactic Unification

Resources

• [Introduction to Unification Theory Lecture 1][itut-1]
• Sections 8.1 and 8.2 of [The Handbook of Automated Reasoning][hoar]

Exercises