chrisdone

How about if instead of data types being represented as type functions, such as,

Foo :: * -> * -> *

we had rows like,

porglezomp

import Data.Fin

%language TypeProviders
%dynamic "./time.so"
%default total

epoch_seconds : IO Int
epoch_seconds = foreign FFI_C "epoch_seconds" (IO Int)

getTime : IO (Provider Int)

Kha

namespace nqueens
open nat

class lt (n : out_param ℕ) (m : ℕ)
instance succ_lt_succ_of_lt (n m) [lt n m] : lt (succ n) (succ m) := by constructor
instance zero_lt_succ (m) : lt 0 (succ m) := by constructor

class ne (n m : ℕ)
instance ne_of_lt (n m) [lt n m] : ne n m := by constructor
instance ne_of_gt (n m) [lt m n] : ne n m := by constructor

rain-1

#lang racket

;; this is a stand alone simple version of the closure conversion part of the hoist pass from the tarot compiler
;; see https://rain-1.github.io/scheme for more.

(require data/queue)

;; closure conversion for lambda calculus
;;
;; the input language is:

deech

import math
proc fizzbuzz(n: int) {.compileTime.} =
  for i in 1 .. n:
    let
      by3 = (i mod 3) == 0
      by5 = (i mod 5) == 0
    if (by3 and by5): echo "FizzBuzz"
    elif by3: echo "Fizz"
    elif by5: echo "Buzz"
    else: echo $i

Icelandjack

Non-standard operators I use :) linked to from my twitter profile

I use kind synonyms

type T   = Type
type TT  = T -> T
type TTT = T -> TT
type C   = Constraint
type TC  = T -> C

AndrasKovacs

{-# language TemplateHaskell, ScopedTypeVariables, RankNTypes,
             TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs,
             TypeOperators, TypeApplications, AllowAmbiguousTypes,
             TypeInType, StandaloneDeriving #-}

import Data.Singletons.TH -- singletons 2.4.1
import Data.Kind

-- some standard stuff for later examples' sake

sordina

// http://journal.stuffwithstuff.com/2013/12/08/babys-first-garbage-collector/
//

#define STACK_MAX 256
#define INITIAL_GC_THRESHOLD 2

#include <stdio.h>
#include <stdlib.h>

void gc(); // Pre-Declared for co-recursive usage

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,_).

r-lyeh-archived

#include <map>  // Component-entity system in 16 lines of C++11. 2013 rlyeh, MIT licensed
#include <set>  // Code fragment from kult engine     -    https://github.com/r-lyeh/kult
enum {JOIN,MERGE,EXCLUDE};using set=std::set<unsigned>;template<typename T> set&system(){
static set entities;return entities;}template<typename T,int MODE>set subsystem(const set
&B){set newset;const set&A=system<T>();if(MODE==MERGE){newset=B;for(auto&id:A)newset.ins\
ert(id);}else if(MODE==EXCLUDE){newset=B;for(auto&id:A)newset.erase(id);}else if(A.size()
<B.size()){for(auto&id:A)if(B.find(id)!=B.end())newset.insert(id);}else{for(auto&id:B)if(
A.find(id)!=A.end())newset.insert(id);}return newset;}template<typename T>std::map<unsig\
ned,T>&components(){static std::map<unsigned,T>objects;return objects;}template<typename\
 T>bool has(unsigned id){return components<T>().find(id)!=components<T>().end();}templat\