notogawa

// gcc -o main main.c -lv4l2
#include <stdio.h>
#include <errno.h>
#include <stdbool.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>
#include <unistd.h>
#include <sys/types.h>
#include <sys/stat.h>

notogawa

// gcc -o main main.c -lv4l2
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <unistd.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <fcntl.h>
#include <libv4l2.h>
#include <linux/videodev2.h>

notogawa

notogawa

#include <stdio.h>
#include <string.h>
#include <stdint.h>
#include <assert.h>
#include <sys/time.h>
#include <sys/ioctl.h>
#include <sys/mman.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <fcntl.h>

notogawa

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Permutation
  ( Permutation(..)

notogawa

module WhatIsInstance where

data Hoge = Foo | Bar

-- 型aが同値関係を持つということを示す型
data ThisIsEq a = ThisIsEq { op :: a -> a -> Bool }

-- 型Hogeが同値関係を持つ証拠となる値
hogeIsEq :: ThisIsEq Hoge
hogeIsEq = ThisIsEq go where

notogawa

#!/bin/env stack
{-
  stack --resolver=lts-12.24 script --package extensible
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}

notogawa

{-# LANGUAGE GADTs #-}
module FooOrBar (someFun, Foo(..), Bar(..)) where

data Foo = Foo deriving Show

data Bar = Bar deriving Show

-- 「a が Foo か Bar である」という命題 (を explicit parameter として扱うため)の定義
data FooOrBarExplicitParameter a where
  IsFoo :: FooOrBarExplicitParameter Foo -- 「a が Foo である」という証明オブジェクト

notogawa

FROM ubuntu:18.04

RUN apt-get update \
 && DEBIAN_FRONTEND=noninteractive \
    apt-get upgrade -y \
 && DEBIAN_FRONTEND=noninteractive \
    apt-get install -y --no-install-recommends \
      haskell-stack \
 && apt-get clean && rm -rf /var/cache/apt/archives/* /var/lib/apt/lists/*

notogawa

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

import Data.Typeable
import Data.Type.Equality
import GHC.TypeLits
import Data.Constraint (Dict(..))