appositum

from functools import partial


class Infix:
    def __init__(self, func):
        self.func = func
    def __or__(self, other):
        return self.func(other)
    def __ror__(self, other):
        return Infix(partial(self.func, other))

appositum

class Pointer(object):
    def __init__(self, target=None):
        self.target = target

    _noarg = object()

    def __call__(self, target=_noarg):
        if target is not self._noarg:
            self.target = target
        return self.target

appositum

const soma = n => {
  sum = n
  const proxy = new Proxy(() => {}, {
    get(obj, key) {
      return () => {
        if (sum) return sum
      }
    },

    apply(receiver, ...args) {

appositum

import qualified Data.Map as M

data Vertex = Vertex String deriving Eq

instance Show Vertex where
  show (Vertex s) = "Vertex " ++ s

type Graph = [(Vertex, [Vertex])]

graph :: Graph

appositum

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}

data ID = A | B | C deriving (Eq, Show)

data Expr = ID ID
          | Expr Expr
          | ID :+: Expr
          | ID :*: Expr

appositum

%               |  casa 1  |  casa 2  |  casa 3  |  casa 4  |  casa 5  |
% cor           |          |          |          |          |          |
% nacionalidade |          |          |          |          |          |
% bebida        |          |          |          |          |          |
% cigarro       |          |          |          |          |          |
% animal        |          |          |          |          |          |

%  1 [x] O Inglês vive na casa Vermelha.
%  2 [x] O Sueco tem Cachorros como animais de estimação.
%  3 [x] O Dinamarquês bebe Chá.

appositum

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE TypeFamilies    #-}
{-# LANGUAGE TypeOperators   #-}

type family TypeEq a b where
  TypeEq a a = True
  TypeEq a b = False

type a /= b = TypeEq a b ~ False

appositum

data ParseError = EndOfStream
                | EmptyInput
                | DoesNotSatisfy

record Parsero s a where
  constructor MkParsero
  parse : s -> (Either ParseError a, s)

Parser : Type -> Type
Parser = Parsero (List Char)

appositum

infixr 5 :>
data Vect : Nat -> Type -> Type where
  Empty : Vect Z a
  (:>)  : a -> Vect n a -> Vect (S n) a

data Sigma : (a : Type) -> (P : a -> Type) -> Type where
  MkSigma : {P : a -> Type} -> (x : a) -> P x -> Sigma a P

vec : Sigma Nat (\n => Vect n Int)
vec = MkSigma 2 (3:>4:>Empty)

appositum

infixr 5 <>
interface VerifiedMonoid (a : Type) where
  mempty : a
  (<>) : a -> a -> a
  leftId : (x : a) -> mempty <> x = x
  rightId : (x : a) -> x <> mempty = x
  assoc : (x : a) -> (y : a) -> (z : a) -> x <> (y <> z) = (x <> y) <> z

[MonoidSum] VerifiedMonoid Nat where
  mempty = 0