emilypi

module Foo

public export
data Foo = Try Int | Again Int

implementation Show Foo where
  show (Try n) = "(Try " ++ (show n) ++ ")"
  show (Again n) = "(Again " ++ (show n) ++ ")"

export

emilypi

;; includes
(add-to-list 'load-path "~/.emacs.d/znc.el")

;; Initialize
(package-initialize)

;; global variables
(setq
 inhibit-startup-screen t
 create-lockfiles nil

emilypi

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes    #-}

module AlaCarte (
  -- newtypes
  Expr,
  -- types
  IntExpr,
  AddExpr,
  Algebra,

emilypi

module Nat (
       -- types
       Algebra
     , Coalgebra
     , NatF
     -- data
     , Fix
     , N
     , Nat
       -- methods

emilypi

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}

module RB where


data F a
  = Lam a (a -> a)
  | Pi a (a -> a)
  | App a a

emilypi

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}

module RB where

import Data.Functor.Contravariant 
newtype O f g e = Comp { deComp :: f (g e) }

newtype Square f a = Square { unSquare :: f (f a) }

emilypi

(use-package haskell-process
  :config
  (custom-set-variables
   '(haskell-process-suggest-remove-import-lines t)
   '(haskell-process-auto-import-loaded-modules t)
   '(haskell-process-log t)
   '(haskell-process-type 'stack-ghci)))

(use-package haskell-interactive-mode
  :hook haskell

emilypi

reverse'' :: Int -> [a] -> [a] -> [a]
reverse'' n [] rs = drop n rs
reverse'' n as rs = h : t
  where 
    h = case as of (a : as) -> head $ reverse'' n as (a : rs)
    t = case as of (a : as) -> reverse'' (n + 1) as (a : rs)

reverse' :: [a] -> [a]
reverse' x = reverse'' 0 x []

emilypi

{-# language RankNTypes #-}
{-# language GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
module Data.Optics where

emilypi

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE GADTs #-}
module Data.Optics where


class Profunctor p where