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

kayceesrk

?- set_prolog_flag(occurs_check,true).

lookup([(X,A)|_],X,A).
lookup([(Y,_)|T],X,A) :- \+ X = Y, lookup(T,X,A).

/* Rules from the STLC lecture */

pred(D,DD) :- D >= 0, DD is D - 1.

type(_,u,unit,D) :- pred(D,_).

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