takanuva

import Control.Concurrent

mergesortM :: (Ord a) => [a] -> IO [a]
mergesortM xs = do
    c <- newChan
    mergesortP xs c
    result <- readChan c
    return result

mergesortP :: (Ord a) => [a] -> Chan [a] -> IO ()

takanuva

{-
    IO operations can be composed through >>=, which is:

        (>>=) :: IO a -> (a -> IO b) -> IO b
    
    The other building block for IOs is the return operation:

        return :: a -> IO a
-}

takanuva

foo = Just (not True)

bar = Just not
-- not :: Bool -> Bool
-- Just :: a -> Maybe a
-- Just not :: Maybe (Bool -> Bool)
--

baz = Just . not
-- Remember that the dot operator joins two functions

takanuva

// Can we write programs without control flow, variables, or even recursion?
// Well, of course we can! Church did that with pen and paper! :)

const to_num = (n) => n((x) => x + 1)(0)

const ZERO = (f) => (x) => x
const ONE = (f) => (x) => f(x)
const TWO = (f) => (x) => f(f(x))
const THREE = (f) => (x) => f(f(f(x)))
const FOUR = (f) => (x) => f(f(f(f(x))))

takanuva

/*******************************************************************************
* Copyright 2022 Paulo Torrens                                                 *
*                                                                              *
* Permission is hereby granted, free of charge, to any person obtaining a copy *
* of this software and associated documentation files (the "Software"), to     *
* deal in the Software without restriction, including without limitation the   *
* rights to use, copy, modify, merge, publish, distribute, sublicense, and/or  *
* sell copies of the Software, and to permit persons to whom the Software is   *
* furnished to do so, subject to the following conditions:                     *
*                                                                              *

takanuva

\/(N: *) ->
\/(z: N) ->
\/(s: N -> N) ->
N

takanuva

-- The language of sorts (S, T, U)
data Sort = Prop
          | SortPi1 String Type Sort
          | SortPi2 String Sort Sort

-- The language of types (A, B, D)
data Type = TypeBound Int
          | TypeApplication1 Type Term
          | TypeApplication2 Type Type
          | TypeLambda1 String Type Type

takanuva

(*
  Prove that, due to the free theorem for impredicative sigma types, strong
  projection is a valid extension. Based on Dan Doel's Agda version:
    https://hub.darcs.net/dolio/agda-share/browse/ParamInduction.agda.
*)

Definition Rel (A: Prop) (B: Prop) :=
  A -> B -> Prop.

Definition Sigma (T: Prop) (U: T -> Prop): Prop :=

takanuva

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
import Control.Monad
import Control.Monad.Trans.Free
import Control.Monad.Trans.Class

--------------------------------------------------

takanuva

#!/bin/bash

# Compile Main for Java bytecode
gcj -C Main.java

# Compile Main for native
gcj -findirect-dispatch -fno-indirect-classes -fpic -c Main.class -o java.o

# Generate header file
gcjh -cp . Main