jonsterling

RACCommand *example = [[RACCommand alloc] initWithSignalBlock:^(id input) { 
  return [RACSignal createWithBlock:^(id<RACSubscriber> subscriber){ 
    [subscriber sendCompleted]; 
    return nil; 
  }];
];

// Now, how will I know when each task has completed?
// I certainly cannot tell from `example.executionSignals.flatten`.

jonsterling

typedef RACSignal *(^RACSignalKleisliBlock)(id input);

@interface RACSignalKleisli : NSObject
- (id)initWithSignalBlock:(RACSignalKleisliBlock)block;
- (instancetype)compose:(RACSignalKleisli *)kleisli;
- (RACSignal *)execute:(id)input;
@end

@implementation RACSignalKleisli {
	RACSignalBlock _signalBlock;

jonsterling

// RACCommand α β === Kleisli RACSignal α β === α -> RACSignal β
// We can pullback along the kleisli arrow to change the input to a command.
// Likewise, we can pushout along the arrow to change the output to a command.


RACSignal *validationSignal = self.form.validationSignal.replayLast;
UIBarButtonItem *doneButton = [[UIBarButtonItem alloc] initWithBarButtonSystemItem:UIBarButtonSystemItemDone target:nil action:nil];
doneButton.rac_command = [self.viewModel.doneCommand ys_pullback:^RACSignal *(id input) {
  return [validationSignal take:1];
}];

jonsterling

brew --config:

HOMEBREW_VERSION: 0.9.4
ORIGIN: https://github.com/mxcl/homebrew.git
HEAD: 0c1bf5fc5158d39e7e83ca2a779c4b4e9a2897fc
HOMEBREW_PREFIX: /usr/local
HOMEBREW_CELLAR: /usr/local/Cellar
CPU: quad-core 64-bit haswell
OS X: 10.8.4-x86_64

jonsterling

1. Install libffi with my modified homebrew formula: https://github.com/jonsterling/homebrew/blob/master/Library/Formula/libffi.rb
2. export PKG_CONFIG_PATH=/usr/local/Cellar/libffi/3.0.13/lib/pkgconfig
3. cabal install libffi
4. cabal install idris

jonsterling

{-# OPTIONS --type-in-type  --no-positivity-check --no-termination-check #-}

module IndexingByCanonicity where

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    π₁ : A
    π₂ : B π₁
open Σ public

jonsterling

Things About Interface Builder in No Particular Order

I have many other problems with Interface Builder beyond the ones here; these are just the ones that immediately came to mind. Likewise, however unsafe I have characterized IB to be in this tract, I assure you, it is far more unsafe than that.

Fragility: stringly styped code strikes again (bite me)

There are a number of places where IB-style stuff encourages unchecked stringly-typed code, and worse, the kind of stringly-typed code that doesn't allow you to use the same constant everywhere to provide some semblance of sanity.

1. Cell reuse identifiers.
2. Storyboard scene identifiers.

jonsterling

{- 
  Given a universe Type with base types in <_> and functions in _~>_, and a language Tm over Type, 
  and decidable equality for types and for terms, we can parse strings of tokens in Tm into trees in Tm.
  We should end up with all possible syntactic interpretations of a given string, but I've not proved this.
  
  Given the following lexicon:
  
    πέδας :: Tm <N>
    ἔβαλε :: Tm (<D> ~> <V>)
    det :: Tm (<N> ~> <D>)

jonsterling

Getting a bit closer to having a typed syntactic parser for Ancient Greek (given a lexicon). Currently, I can infer MERGE types (direction and application vs. composition), but it still requires some hints as to constituency in cases where the structure is not all nesting in one direction.

So the following string gets parsed perfectly without any help:

τὴν Εὐρυτείαν οἶσθα δῆτα παρθένον

But something like the following needs some brackets to help the parser understand what's up:

ναυμαχία [ γίγνεται [{∅-adv} ἐπ' {∅-det.} Αἰγίνῃ] {∅-det} μεγάλη]

jonsterling

module dingle where
  open import Data.String using (String)
  open import Relation.Binary.PropositionalEquality using (_≡_; refl)

  module Theory (rep : Set) where

    infixr 0 _⇒_
    data * : Set where
      ⟨_⟩ : rep → *
      _⇒_ : * → * → *