#1. Fin n の構築子(constructor)が Data/Nat.agda の ℕ と同じく zero と suc （で混乱する可能性）
#2. 1. で挙げた名前の衝突の解決のために、Data/Fin.agda は Agda の文法 module の機能 as と using を使う。この機構は Haskell にもある : import qualified と import M (blah) だから、ここでは躓かないかな？
#3. data Fin : ℕ → Set where ... が有限集合に対応することが直観的でない（わかればわかる的なにか）
##3です
#そもそも fzero : {n : Nat} -> Fin (suc n)となってて、nが暗黙でありながら、Fin (suc n)って使われててナニコレ？でした
#fzero : Fin zeroの間違いでは？と思ってたんですが、完全に勘違い。
#私の場合にはGADTsなんだということを再確認したらよかっただけなのですが。
#Fin 0 は立ち止まるところだと思います。そこはおいといて、Fin 2 とか Fin 3 とかを具体的に手を動かすとなるほどという
#Fin 0を作れるような構成子はないし、Fin 1を作れるのはfzeroのみ、と。
#はい
#そうですね。
#fzero : Fin 1もあるしfzero : Fin 2もあるし、そういうものだという風に見えてなかったです。
#ひとつずつ具体例で考えると分かったので、やはり私はまだ「わかりやすいように抽象的に話してくれ」とはならなそうです。
#そういう意味ではつまずいてたのは1,3の両方かな。
#週末An Introduction to Dependent Types and Agda (Andreas Abel)を読んでましたが、ここのところ同じような説明ばっか何度も読んでる気がする。
#これは理解しつつあるのか、それとも慣れ始めただけなのか。
#ghc 7.6.3 でてます
#一般人にはHPが出てることが重要でござる。
#おっしゃるとおりです…
#http://p.tl/g1Zd 第7回IFPH読書会の案内です。ちょっと空いて6/2(sun)になります。 #Universeの文脈に出てくるcodeとかdecodeって何なんでしょう？ A universe is a type of codes together with an interpretation
function that computes types from codes:
#あるいは、A universe is a set of types (or type formers) and a universe construction consists ofa type of codes and a decoding function mapping codes to type in the universe.
#The purposeof a universe construction is to be able to define functions over the types of the universe by inspecting their codes.
#ぼくもわからんので、freenode #agda で質問をしています。識者はわかっているらしい。
#覗いてみよう
# 
haskell-ja > Archives > 2013/04/22