haitlahcen

module Main

%default total

infixr 20 <>

StackType : Type
StackType = List Type

data Stack : List Type -> Type where

haitlahcen

(Lam Nat:*. 
 Lam s:Nat -> Nat. 
 Lam z:Nat. 
 Lam fold:Nat -> Pi R:*. (R -> R) -> R -> R. 
 Lam A:*.
 Lam x:A.
 fold (s (s (s (s z)))) A (Lam x:A. x) x)
(Pi Nat:*. (Nat -> Nat) -> Nat -> Nat)
(Lam Number:Pi N:*. (N -> N) -> N -> N.
 Lam Nat:*.

haitlahcen

-- TypeChecker.hs ---
-- Copyright (C) 2018 Hussein Ait-Lahcen
-- Author: Hussein Ait-Lahcen <[email protected]>
-- This program is free software; you can redistribute it and/or
-- modify it under the terms of the GNU General Public License
-- as published by the Free Software Foundation; either version 3
-- of the License, or (at your option) any later version.
-- This program is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the

haitlahcen

(Lam Object:**.

 Lam Hom: Object -> Object -> *.

 Lam identity: Pi A:Object. Hom A A.

 Lam compose: Pi A:Object.
              Pi B:Object.
              Pi C:Object.
              Pi AB:Hom A B.

haitlahcen

let

  Eq:Pi A:*. (A -> A -> *) =
    Lam A:*.
    Lam x:A.
    Lam y:A.
    Pi Prop:A -> *.
    (Prop x) -> (Prop y),

  Refl:Pi A:*. Pi x:A. (Eq A x x) =

haitlahcen

==================== FINAL INTERFACE ====================
2019-01-22 10:12:16.006575114 UTC

interface main:DB.QueryLineSpecs 8044
  interface hash: d03191514f73c041eb6604fb6258090c
  ABI hash: e0b08fb5b41eabcd21eb03791960814a
  export-list hash: 1f51434d86438386375a39f852e60287
  orphan hash: f2f94d0ba3bb20cd4cc684b4de178bd4
  flag hash: 8ba54d655c55d48965b87370f5486c43

haitlahcen

# ======================================== header.h =============================================
#define TRUE 1

# ======================================== X.hs =================================================
module X where

x = 1

# ======================================== Test.hs ==============================================

haitlahcen

module Main where

import           Control.Monad      (replicateM, replicateM_, when)
import           Data.Binary
import           Data.Binary.Get    (bytesRead, getInt64be, getWord32be,
                                     getWord64be, getWord8, lookAhead, skip)
import           Data.Bool          (bool)
import           Data.Char          (chr)
import           Data.Functor       (void, ($>))
import           Data.List          (find)

haitlahcen

App

(>>=) :: m a -> (a -> m b) -> m b
(<$>) :: (a -> b) -> f a -> f b

Very hard to understand that both functions are similar in their essence.

haitlahcen

#! /usr/bin/env nix-shell
#! nix-shell --pure -i runghc -p "ghc.withPackages (ps: with ps; [ tagged bifunctors ])"

{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}

module Main where

import Data.Tagged
import Data.Functor.Sum