enolan

# For more information, see: http://docs.haskellstack.org/en/stable/yaml_configuration.html

# Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2)
resolver: lts-4.2

# Local packages, usually specified by relative directory name
packages:
- '.'

# Packages to be pulled from upstream that are not in the resolver (e.g., acme-missiles-0.3)

enolan

import Decidable.Equality
%default total

AtLeastTwo : Type -> Type
AtLeastTwo ty = Sigma (ty,ty) (\(a,b) => Not (a = b))

atLeastTwoNats : AtLeastTwo Nat
atLeastTwoNats = ((0,1) ** absurd)

atLeastTwoBools : AtLeastTwo Bool

enolan

Haskell: The Bad Parts
Complaining about a tiny program, armchair language design

What's the program? Pia-forward
A utility for setting up port forwarding on the Private Internet Access VPN service
- 103 lines
- Mostly IO
- Deals with exceptions
- JSON
- web service API

enolan

%default total
-- What's Idris?
-- * Dependently typed
-- * purely functional
-- * haskell-like syntax
-- Looks like this:

bottles : Nat -> String
bottles    Z    = "Buy more beer!"
bottles n@(S k) = show n ++

enolan

Tue Oct  6 16:59:24 PDT 2009  Echo Nolan <echo@echonolan.net>
  * Fix Iter.take delaying actions one step.
  It was broken in two maddeninly subtle ways. The first: using joinIM delayed
  all actions associated with take's parameter iteratee one step. The second:
  it always returned Cont when the length of the chunk was <= the requested
  length and non-null. Thus, the values returned were one step delayed if the
  amount to take was equal to the length of the chunk passed.

New patches:

enolan

{-
Read from a tcp socket and copy the stream to stdout using iteratee-based I/O.
To try this: in GHCI, run testEnumSocket; in another terminal, run
'nc localhost 31337'. Anything typed in the netcat terminal will show up in the
GHCI terminal. Go nuts!
Needs network-bytestring and iteratee from Hackage.
-}
module IterateeNetcat where
 
import qualified Data.ByteString as B

enolan

; Goal: Turn Array `["foo", "bar", "baz"]` into String `"ordered: 1=foo 2=bar 3=baz"`.

; Clojure

;; Read arguments from command line
;; (def argv *command-line-args*)

;; Fake command-line arguments for use in REPL
(def argv (seque ["foo" "bar" "baz"]))

enolan

data BEncode = BInt Integer
	     | BString ByteString
	     | BList [BEncode]
             | BDict (Map ByteString BEncode)
	       deriving (Eq, Ord, Show)

getInt i = case i of
    BInt i' -> Just i'
    _       -> Nothing
getString s = case s of

enolan

# Modified for pulseaudio by Echo Nolan <echo@echonolan.net>
# Contributor: Slumslayer <paul.smet [at] gmail [dot] com>
# Original Contributor: Fabio Linux <fbo.linux [at] gmail [dot] com>

pkgname=mplayer-nogui-pulse
pkgver=28347
pkgrel=4
pkgdesc="A movie player for linux"
arch=(i686 x86_64)
depends=('libxxf86dga' 'libxv' 'libgl' 'faac' 'ttf-dejavu')

enolan

Keybase proof

I hereby claim:

• I am enolan on github.
• I am enolan (https://keybase.io/enolan) on keybase.
• I have a public key whose fingerprint is 98FE 410B F035 E5A9 CEFD 7909 7B01 2803 D27E 62E3

To claim this, I am signing this object: