brunoczim

module Data.Tree where

data BinTree a
  = Leaf
  | Branch
    { binTreeLeft :: BinTree a
    , binTreeNode :: a
    , binTreeRight :: BinTree a
    }
  deriving (Show, Read, Eq, Ord)

brunoczim

module Binomial
  ( fact
  , comb
  , prob
  , probs
  , weights
  , expected
  , mean
  , squaredDev
  , variance

brunoczim

module Approx where

approxGolden :: Int -> Double
approxGolden n = approx n 1 1
  where
    approx 0 p q = q / p
    approx n p q = approx (n - 1) q (p + q)

golden :: Double
golden = approxGolden 64

brunoczim

module Tuple

open import Data.Vec
open import Agda.Builtin.Nat renaming (Nat to ℕ)

data Tuple : {n : ℕ} → Vec Set n → Set where
  ∅   : Tuple []
  _,_ : {A : Set} {n : ℕ} {v : Vec Set n} → A → Tuple v → Tuple (A ∷ v)

brunoczim

module Curry where

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    andL : A
    andR : B

curry : {A B C : Set} → (A × B → C) → (A → B → C)
curry f = λ {x y → f (x , y)}

brunoczim

{-# LANGUAGE FlexibleInstances #-}

module Main where

import Data.String (IsString, fromString)


-- language types
-- 1. integers
-- 2. string

brunoczim

{-# LANGUAGE ScopedTypeVariables, EmptyCase #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

module CurryHoward where

type Unit = ()
data Void

type And a b = (a, b)
data Or a b = OrL a | OrR b

brunoczim

Introdução aos Tipos Dependentes

Overview

No mundo da programação funcional, uma ideia introduzida há algum tempo vem ganahando força. É a tipagem dependente: tipos que dependem de valores. O tipo de par ordenado (n : Natural) ⨯ (Vetor a n) é um exemplo de tipo dependente. O primeiro elemento do par é um número natural n. O segundo elemento é um vetor que armazena valores do tipo a e cujo tamanho é aquele mesmo número natural n. Estabelecemos uma relação de dependência entre um tipo e um valor. O primeiro elemento do par é sempre o tamanho do vetor.

brunoczim

use std::{
    cmp::Ordering,
    fmt,
    hash::{Hash, Hasher},
    ops::{
        Index,
        Range,
        RangeFrom,
        RangeFull,
        RangeInclusive,

brunoczim

module Sorting where

-- tail recursive, much better performance
sort :: Ord a => [a] -> [a]
sort xs = loop [xs] [] where
  loop [] ys = ys
  loop ([] : xss) ys = loop xss ys
  loop ((x : xs) : xss) [] = loop (xs : xss) [x]
  loop ((x : xs) : xss) (y : ys) = if x <= y
    then loop (xs : xss) (x : y : ys)