About Cosense
Help
Log in
mrsekut-p
E
x
i
s
t
e
n
t
i
a
l
Q
u
a
n
t
i
f
i
c
a
t
i
o
n
型
に
量
化
子
を
付
け
ら
れ
る
よ
う
に
す
る
G
H
C
拡
張
殆
ど
の
場
合
(
常
に
?
)
存
在
型
を
定
義
す
る
た
め
に
使
う
こ
う
い
う
普
通
に
全
称
量
化
の
為
に
使
用
す
る
こ
と
も
で
き
る
っ
ち
ゃ
で
き
る
の
で
、
「
存
在
型
を
使
う
た
め
の
拡
張
」
と
い
う
説
明
が
適
当
な
の
か
わ
か
ら
な
い
mrsekut
h
a
s
k
e
l
l
{
-
#
L
A
N
G
U
A
G
E
E
x
i
s
t
e
n
t
i
a
l
Q
u
a
n
t
i
f
i
c
a
t
i
o
n
#
-
}
i
d
:
:
f
o
r
a
l
l
a
.
a
-
>
a
i
d
a
=
a
冗
長
に
な
っ
て
い
る
だ
け
な
の
で
何
も
嬉
し
く
な
い
け
ど
mrsekut
Related
Sort by
Related
Modified
Created
Last visited
Most linked
Page rank
Title
Links
存在型
[/ Existential type][存在型のどのへんが存在量化なのか]こういうことをできる型`data Hoge = forall x. Hoge x`左辺の引数に取らない型を、右辺で使用する
GHC拡張
[GHC]の拡張Haskell98やHaskell2010の仕様を拡張した機能を使えるプラグマ`{-# LANGUAGE HogeHoge #-}`で指定する[docs https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts.html]分類もされている
Open Union
拡張可能(Open)な、Union型a type-indexed coproduct of functorsと、[『Extensible Effects An Alternative to Monad Transformers』]に書いてた[open-union]https://hackage.haskell.org/package/open-union
GHC拡張一覧
from [GHC拡張][Safe Haskell Extensions]や[Haskell Language Standard Extensions]も含むGHC v9.0.1で見ている「消えた?」みたいなコメントはこれに対して言っているできればもっと細かく分類したい[mrsekut.icon]
存在型のどのへんが存在量化なのか
特にHaskellの[存在型]についてわかりにくい点存在量化の話をしているはずなのに`forall`というキーワードを使っている基本的にはこれに尽きる[mrsekut.icon]でもまあ実際、`forall`を導入するだけで存在型を作れちゃうわけだから仕方がない
QuickCheck
[Property based testing]をする[docs https://hackage.haskell.org/package/QuickCheck-2.13.2/docs/Test-QuickCheck.html]代表的な関数の紹介 [ref https://haskell.e-bigmoon.com/stack/test/quickcheck.html]導入`package.yaml`のdependenciesに`QuickCheck`を追記
GHC拡張
Haskellに纏わるツールたち
#俯瞰Haskellに纏わるツールたちを3行で説明する多すぎでは?キレそう[mrsekut.icon][Haskellの環境構築]ビルドツール
型クラス
その型が持つべき性質を定義する型のinterfaceになる[Ad Hoc多相]Scala, PureScriptにもある[MultiParamTypeClasses]という[GHC拡張]がある
RequiredTypeArguments
https://zenn.dev/mod_poppo/articles/playing-with-visible-forall[GHC-9.10]で実装された可視なforallで遊ぶ`{-# LANGUAGE RequiredTypeArguments #-}``-- 普通の id 関数``id :: forall a. a -> a`
LinearTypes
[Haskell]で[線形型]をする[GHC拡張][GHC-9.0.1]から使える[docs https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html][proposal https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst]
PostfixOperators
`(10!)`とか`(10%)`のように、引数の後に関数を書く記述ができる[GHC拡張]
TypeFamilies
[Type Family]を扱う[GHC拡張]以下の拡張を含む[MonoLocalBinds][KindSignatures][ExplicitNamespaces]
ConstraintKinds
型エイリアスと同じ構文で、[型制約種]のエイリアスを書くことができる[GHC拡張]例`{-# LANGUAGE ConstraintKinds #-}``-- 型制約のエイリアス``type MonMonad m a = (Monoid (m a), Monad m) -- :: Constraint`
DataKinds
以下のような昇格ができる[GHC拡張][型コンストラクタ]→[kind][値コンストラクタ]→[型コンストラクタ]GHC v7.4.1で入った`data Nat = Zero | Succ Nat`のような型を定義したとき
kind
日本語では「種」と言う読み方わからないが[「しゅ」っぽい https://twitter.com/mrsekut/status/1238871776043470849]型の型[型コンストラクタ]の型のようなもの`:k`、`:kind`で調べられる
GHC
[/ Glasgow Haskell Compiler][University of Glasgow]が作ったHaskellのコンパイラ[Haskell]のコンパイラとインタプリタHaskell98やHaskell2010の仕様に沿っている他のコンパイラには、UHCやLHCというのがあるらしい
ghci
[GHC]のインタプリタ以下の`:hoge`のようなコマンドは、一文字で`:h`のように省略可能`$ stack ghci``$ stack ghci --no-load`[docs https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/ghci.html]
多相関数
[parametric polymorphic function][generic function][多相型]を持つ関数普通のHaskellの任意の型は関数全体に`forall`が暗黙的に付いている`length :: [a] -> Int -- これは`
PartialTypeSignatures
[GHC-7.10.1]型シグネチャ版の[Type-Holes]型シグネチャ内にワイルドカード(`_`)を書ける[GHC拡張]通常の[Type-Holes]は、式部分にワイルドカードを使うが、PartialTypeSignaturesは型シグネチャ部分にワイルドカードを使える
GHC 2021
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0380-ghc2021.rst[GHC拡張]の多くもdefaultで取り込まれるのか[mrsekut.icon]https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0372-ghc-extensions.rst#motivation
package.yaml
[Stack]の追加libaryの指定など追加のlibararyの指定などは[.cabal]ではなく、package.yamlに書く[hpack(Haskell)]が自動で変換してくれる[hpack(Haskell)]を使いたくない場合は、package.yamlを削除して、[.cabal]に書けばいいパッケージを追加したいときは`dependencies:`以下に追加していけばいい
TypeFamilyDependencies
from [Type Family][GHC拡張]>#WIPただの[TypeFamilies]だけでは単射になっていないから、どんな問題が起こる #??
KindSignatures
[kind注釈]をつけられる[GHC拡張]無くても[kind推論]されるが可読性のために付けたいkind推論に失敗するので付けたいというケースもある #??あるなら具体例を見たい[mrsekut.icon]
DeriveGeneric
from [GHC拡張][Generic型クラス]のderivingを可能にするつまり`deriving Generic` って書ける
MonadComprehensions
from [GHC拡張]https://kowainik.github.io/posts/arrows-zoo#comprehensionListモナド以外のMonadでも[リスト内包表記 (hs)]を書ける
GHCのPragma
`{-# HOGE #-}`って書くやつLANGUAGE[GHC拡張]の導入UNPACKhttps://stackoverflow.com/questions/33931991/what-does-the-unpack-pragma-do-in-this-case
FunctionalDependencies
[Functional Dependencies]をやる[GHC拡張]GHC 6.8.1から入ったhttps://wiki.haskell.org/GHC/AdvancedOverlap直接は関係ないが似たような話
OverlappingInstances
[GHC拡張]https://myuon.github.io/posts/overlapping-instances/[OVERLAPPINGプラグマ][OVERLAPPABLEプラグマ][OVERLAPSプラグマ]
存在型
戻り値でのimpl Trait
from [impl Trait][存在型][RFC 1522 https://github.com/rust-lang/rfcs/blob/master/text/1522-conservative-impl-trait.md]例`fn f() -> impl Iterator<Item = i32> {`
TaPL
関数に対してDI
from [DI]>#WIPhttps://fsharpforfunandprofit.com/posts/convenience-functions-as-interfaces/案カリー化する
STANDARDIZED OPEN LADDER OF FUNCTIONAL PROGRAMMING
GHC.TypeNats
https://hackage.haskell.org/package/base-4.15.0.0/docs/GHC-TypeNats.html[SomeNat型]https://qiita.com/mod_poppo/items/3a37424d299a9f71b757#実行時の値を型レベル自然数に持ち上げる[存在型]よりcompilerに近いmoduleといった感じかな[mrsekut.icon]
『Thinking with Types』
『(展望)17 モデルと表現』
幽霊型とrank-2 typesで型安全なスコープを作る
>#WIPタイトルが雑なので直す[mrsekut.icon]幽霊型とrank-2 typesを組み合わせたテクニックスコープを作るのに使っている?[『Ghosts of Departed Proofs』]と[STモナド]で見かけた[mrsekut.icon]
Data.Exists
[PureScript]で[存在型]をするmodule[pursuit https://pursuit.purescript.org/packages/purescript-exists/5.0.0/docs/Data.Exists]>使い方https://qiita.com/acple@github/items/216542d1c4844c2ec879
Stack Safety for Free
[PureScript]で[Stack Over Flow]を起こさない[Freeモナド]の実装に関する[論文][Phil Freeman]著2015/8/8[PDF http://functorial.com/stack-safety-for-free/index.pdf]#論文メモ
Created
5 years ago
by
mrsekut
Updated
4 years ago
by
mrsekut
Views: 35
Page rank: 7.6
Copy link
Copy readable link
Start presentation
Hide dots
ExistentialQuantification
型に量化子を付けられるようにする
GHC拡張
殆どの場合(常に?)
存在型
を定義するために使う
こういう普通に全称量化の為に使用することもできるっちゃできるので、「存在型を使うための拡張」という説明が適当なのかわからない
mrsekut.icon
code:hs
{-# LANGUAGE ExistentialQuantification
#-}
id :: forall a. a -> a
id a = a
冗長になっているだけなので何も嬉しくないけど
mrsekut.icon