jonsterling

NSString *safe = self.keys.url.port.stringValue;
NSString *unsafe = @"url.port.stringValue";
assert([safe isEqualToString:unsafe]);

jonsterling

Pod::Spec.new do |s|
  s.summary = 'A simple iPhone forms library'
  s.license = 'Apache License, Version 2.0'
  s.source = { :git => 'https://github.com/yardsale/IBAForms.git', :tag => '1.1.0' }
  s.source_files = 'library/**/*.{h,m}'
  s.author = { 'Itty Bitty Apps' => 'info@ittybittyapps.com' }
  s.version = '1.0.0'
  s.homepage = 'https://github.com/ittybittydude/IBAForms'
  s.name = 'IBAForms'
  s.platform = :ios

jonsterling

module Main where

import System.FilePath
import System.Process
import System.Exit
import System.Environment
import Control.Applicative

import Control.Monad.Identity

jonsterling

#!/usr/bin/python
# -*- coding: latin-1 -*-

import urwid
import json
import subprocess

class TaskWarrior(object):

    def pending_tasks(self):

jonsterling

// Which of these do you find easier to scan?

// This is what I imagine you would prefer. No single-char variable
// names. The purpose of every variable is described to the best of my
// ability, though many parameters are just that: parameters.

implicit def KleisliCategory[MonadParam[_]: Monad]: 
    Category[({type TypeConstructor[FirstParam,
SecondParam] = Kleisli[MonadParam, FirstParam,
SecondParam])#TypeConstructor] = new Category[({type

jonsterling

ἔγωγε δὲ φοβοῦμαι, ὦ ἄνδρες, μὴ ἂν εἴη καὶ Δημοσθένης τις ἀδύνατος εἰπεῖν τὴν τῶν ἀδικημάτων δεινότην τῶν τρίακοντα· οὐ γὰρ μόνον ἀπέκτειναν τοὺς ἀναιτίους ὧντινων αἱρήσονται τὰ χρήματα, ἀλλὰ καὶ εἰς τοσοῦτον ἧκον αἰτίας ὥστε προὔδωκαν τοὺς τε φίλους καὶ τοὺς προσήκοντας θᾶττον ἢ τοὺς ἔχθρους. τοσαύτη γὰρ οὖν ἡ μοχθηρία τούτων ὥστε διήρπασάν ποτε οἱ τριάκοντα καὶ τοὺς σφετέρους.

I am afraid that even a Demosthenes would be unable to express the heinousness of the crimes of the Thirty. Not only did they kill the innocent in order to take their money, but they reached such a level of criminal behavior that they betrayed their own friends and relations even more quickly than their enemies. In fact, their corruption was so extensive that the Thirty began to prey upon their own members.

(To be clear, I composed the Greek from the English. Not the other way around.)

jonsterling

-- Inspired by http://www2.tcs.ifi.lmu.de/~abel/popl13.pdf

[codata|
  codata Stream a where
    head :: Stream a -> a
    tail :: Stream a -> Stream a
|]

fib :: Stream Nat
[copattern|

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 → *
      _⇒_ : * → * → *

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

{- 
  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>)