damhiya

let and = fn (b1 : bool) -> fn (b2 : bool) ->
            if b1 then b2 else false in
let or =  fn (b1 : bool) -> fn (b2 : bool) ->
            if b1 then true else b2 in
let map = fn (f : int * int * int -> int * int * int) ->
          fix (mapf : list (int * int * int) -> list (int * int * int)) xs ->
            case xs of
              { [] -> [] of (int * int * int)
              ; x :: xs -> f x :: mapf xs
              } in

damhiya

# Tetrahedron
# volume = 1/6
# area = (3 + sqrt 3)/2

tetrahedronMesh =
    let vmap = [ 0. 1. 0. 0.
               ; 0. 0. 1. 0.
               ; 0. 0. 0. 1.
               ]
        fmap = [ 0 0 0 1

damhiya

회전

회전에 대해 알아보자. 2차원에선 간단하지. 점 $(x,y)$를 $\theta$만큼 회전시킨 좌표 $(x',y')$은 이렇게 표현이 돼.

$$ \begin{pmatrix} x' \ y' \end{pmatrix} = \begin{pmatrix} \cos \theta & \sin \theta \

damhiya

#!/usr/bin/env bash
PROFILE_PATH=/nix/var/nix/profiles

get_list() {
  find $PROFILE_PATH -type l \
  | awk "match(\$0, /^${PROFILE_PATH//\//\\\/}\/system-([0-9]*)-link\$/, res) { print res[1] }" \
  | sort
}

get_current() {

damhiya

{
  inputs = {
    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
    flake-utils.url = "github:numtide/flake-utils";
  };

  outputs = { self, nixpkgs, flake-utils }:
    flake-utils.lib.eachDefaultSystem (system:
      let
        pkgs = import nixpkgs { inherit system; };

damhiya

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs          #-}

module Main where

import GHC.Types
import Control.Monad

type Coffee = Integer
type Work = Integer

damhiya

{-# LANGUAGE ExplicitForAll      #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Rose where

data Tree a = Node a [Tree a] deriving (Eq, Show)

t1 :: Tree Int
t1 = Node 1
       [ Node 2

damhiya

{ stdenv, coq }:
stdenv.mkDerivation {
  pname = "coq${coq.coq-version}-coq-menhirlib";
  version = "20211125";
  src = builtins.fetchTarball {
    url = "https://gitlab.inria.fr/fpottier/menhir/-/archive/20211125/archive.tar.gz";
    sha256 = "0ls13myx5g4d32rq5prnikql0wvsrisll88xhbwi3w9v13lwnal0";
  };
  buildInputs = [ coq ];

damhiya

fmap2 :: (Functor f1, Functor f2) => (a -> b) -> f1 (f2 a) -> f1 (f2 b)
fmap2 = fmap . fmap

for :: Functor f => f a -> (a -> b) -> f b
for = flip fmap

infixr $:
($:) :: (Functor f, Functor g) => f (g a) -> (a -> b) -> f (g b)
($:) = flip fmap2

damhiya

{-# LANGUAGE StandaloneDeriving     #-}
{-# LANGUAGE DeriveFunctor          #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PatternSynonyms        #-}
{-# LANGUAGE ViewPatterns           #-}
{-# LANGUAGE LambdaCase             #-}

module Fibonacci where