Skip to content

Instantly share code, notes, and snippets.

@JadenGeller
JadenGeller / Type-Level Assertions.swift
Last active March 9, 2018 03:06
Type-Level Assertions (or, almost-dependent types)
/*
* We've defined "traits" by which we can type an integer that are characteristic of its value.
* These traits can even be subtraits of other traits (like both positive and negative being nonzero).
*
* We can use these traits in the type signatures of functions to indicate what trait will be returned
* as a function of the passed-in traits.
*
* Even cooler, we can specify properties of the traits such that we can runtime-verify the correctness
* of these labels (in case a function was improperly annotated, for example).
*/
@david-christiansen
david-christiansen / FizzBuzzC.idr
Last active August 29, 2022 20:00
Dependently typed FizzBuzz, now with 30% more constructive thinking
module FizzBuzzC
%default total
-- Dependently typed FizzBuzz, constructively
-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
ZeroFizzy : Fizzy 0
Fizz : Fizzy n -> Fizzy (3 + n)
@mxswd
mxswd / TypeNats.swift
Last active December 12, 2016 19:24
Thanks @robrix and CodaFi_ for the discussion :D
// this is a playground
protocol Nat {
class func construct() -> Self
class func value() -> Int
}
struct Z : Nat {
static func construct() -> Z {
return Z()
}
__attribute__((format_arg(__NSString__, 2)))
NSString *ಠ_ಠ_message(const char *severity, const char *format) {
return [NSString stringWithFormat:@"%s: %s", severity, format];
}
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Wformat-nonliteral"
__attribute__((format(printf, 1, 2)))
void ಠ_ಠ_warning(const char *format, ...) {
va_list ಠ_ಠ;
va_start(ಠ_ಠ, format);
@CodaFi
CodaFi / Accelerando
Last active December 14, 2015 17:38
ACCELERATE(x) _mm_set1_ps((float)&x)
DECCELERATE_INTO(x, f) _mm_store_ss(&f, result)
Sample usage:
//accelerate a float into a super-fast 128 mm register
float x = 1.0f;
__m128 vecX = ACCELERATE(x);
//deccelerate a 128 mm register value back to a float
@jwilling
jwilling / CustomClipView.m
Last active October 12, 2015 09:08
NSTableView with custom clip view
- (id)initWithFrame:(NSRect)frame {
self = [super initWithFrame:frame];
if (!self) return nil;
self.layer = [CAScrollLayer layer];
self.wantsLayer = YES;
self.layerContentsRedrawPolicy = NSViewLayerContentsRedrawNever;
return self;
}