notogawa

module C where

import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; refl)

data C {A : Set} : Set where
  c : (a : A) → C

------ ケース1
-- OK

notogawa

function init-prompt-git-branch()
{
  git symbolic-ref HEAD 2>/dev/null >/dev/null &&
  echo "($(git symbolic-ref HEAD 2>/dev/null | sed 's/^refs\/heads\///'))"
}

if which git 2>/dev/null >/dev/null
then
  export PS1_GIT_BRANCH='\[\e[$[COLUMNS]D\]\[\e[1;31m\]\[\e[$[COLUMNS-$(length $(init-prompt-git-branch))]C\]$(init-prompt-git-branch)\[\e[$[COLUMNS]D\]\[\e[0m\]'
else

notogawa

ghc-8.2.1-rc1でcabal-installを試すにはcabalのリポジトリe4c36b9dd時点に， このパッチ当てて

EXTRA_CONFIGURE_OPTS="--allow-newer=base,time" ./bootstrap.sh

あと，配布されてる ghc-8.2.0.20170404-x86_64-deb8-linux.tar.xz はjesssieだとリンクに失敗するのでsidにしとくといい

notogawa

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Siri where

import GHC.TypeLits (Nat)

notogawa

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
module Main where

import Prelude hiding ((.), Word)
import qualified Prelude
import Data.Singletons

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(..))

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 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

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

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