pelotom

-- Informal proof:
--==============================================================
--  S a * (b + c)
--= b + c + a * (b + c)         -- definition of *
--= b + c + (a * b) + (a * c)   -- induction hypothesis
--= b + (a * b) + c + (a * c)   -- associativity / commutativity
--= S a * b + S a * c           -- definition of *

-- With all associativity and commutativity manipulations:
--==============================================================

pelotom

-- Axioms
rec_N :
  (P : Nat -> Type) ->
  (ind : (n : Nat) -> P n -> P (S n)) ->
  (base : P Z) ->
  (m : Nat) ->
  P m
Even : (n : Nat) -> Type
Odd : (n : Nat) -> Type
zeroIsEven : Even Z

pelotom

curry : {A : Type}
     -> {B : A -> Type}
     -> {C : Sigma A B -> Type}
     -> ((p : Sigma A B) -> C p)
     -> (x : A) -> (y : B x) -> C (x ** y)
curry f x y = f (x ** y)

-- Dependent uncurry is just the induction principle for sigma types
uncurry : {A : Type}
       -> {B : A -> Type}

pelotom

public class JavaGenTest {

  public static interface F<a, b> {
    b f(a a);
  }

  public static abstract class P2<a, b> {
    private static final class _P2<a, b> extends P2<a, b> {
      private final a _1;
      private final b _2;

pelotom

data ABList a b = Cons a (ABList b a) | Nil
  deriving Show
  
zipAB :: [a] -> [b] -> ABList a b
zipAB [] _ = Nil
zipAB (a:as) bs = Cons a (zipAB bs as)

-- > zipAB [1..] "hey"
-- Cons 1 (Cons 'h' (Cons 2 (Cons 'e' (Cons 3 (Cons 'y' (Cons 4 Nil))))))

pelotom

$ git push heroku master
Counting objects: 46, done.
Delta compression using up to 8 threads.
Compressing objects: 100% (40/40), done.
Writing objects: 100% (46/46), 53.45 KiB, done.
Total 46 (delta 0), reused 0 (delta 0)

-----> Fetching custom git buildpack... done
-----> Haskell app detected
-----> Downloading GHC

pelotom

scala> import scalaz._, Scalaz._, Unapply._
import scalaz._
import Scalaz._
import Unapply._

scala> List(1, 2, 3).traverseU((i: Int) => i.pure[({type f[a] = State[Int, a]})#f])
<console>:17: error: Unable to unapply type `scalaz.IndexedStateT[[+X]X,Int,Int,Int]` into a type constructor of kind `M[_]` that is classified by the type class `scalaz.Applicative`
1) Check that the type class is defined by compiling `implicitly[scalaz.Applicative[<type constructor>]]`.
2) Review the implicits in object Unapply, which only cover common type 'shapes'
(implicit not found: scalaz.Unapply[scalaz.Applicative, scalaz.IndexedStateT[[+X]X,Int,Int,Int]])

pelotom

import effectful._
import scalaz._
import Scalaz._
import effect._
import ST._
import std.indexedSeq._

def fibST(n: Int): List[Int] = {
  type ForallST[A] = Forall[({type λ[S] = ST[S, A]})#λ]

pelotom

Brouwer's philosophy of language starts from the conviction that direct
communication between human brings is impossible. His chapter on "Language"
in "Life, Art and Mysticism" starts as follows: "From Life in the Mind
follows the impossibility of communicating directly with others... Never
has anyone been able to communicate directly with others soul-to-soul."
The privacy of mind and thought and and the hypothetical existence of minds
in other human beings, who are no more than the Subject's mind-creations,
"things in the exterior world of the Subject" rule out "any exchange of
thought".

pelotom

public static abstract class List<a> {
    private static final class $Nil<a> extends List<a> {
        private $Nil() {
        }

        public <M> M match(final M $ifNil, final $F<a, $F<List<a>, M>> $ifCons) {
            return $ifNil;
        }
    }