haskell-jp / questions #12

ExplicitForAll の方が ScopedTypeVariables よりも導入が後だった気がする。
appveyorで、バイナリを作りたいのですが、できあがったバイナリがどこにあるのか分かりません。どなたか、どう記述すればいいか、ご存知ありませんか?
github からとってきたソースは C:\projects\<packagename> にあって、stack はここで実行される。
stack が作業に使うのは、stack_root にしていしたディレクトリ。
artifacts は、前者内での相対パスしか使えないので、バイナリが見えない。
stack --local-bin-path . install <package_name> すると、作業ディレクトリから後者へバイナリをコピーしてくれる。
やった! <- 今ココ
う、スレッドになってなかった。ごめんなさい。
Copying from C:\projects\hs-tls\.stack-work\install\1e01afab\bin\tls-simpleclient.exe to C:\projects\hs-tls\tls-simpleclient.exe

きたー!
ちょっとHaskellと外れた質問かな、と思いきや、なるほどAppVeyorではなくstackの使用についての質問でしたか。。。すみません、察せなくて。
実行時の数値からNat種の型を作る(?)には GHC.TypeLitssomeNatVal 関数などを使えばできるとおもうのですが、この時作られる型を自作の型クラスのインスタンスに限定するにはどのようにすればいいのでしょうか?:sob::sob::innocent:
補足します:man-bowing::writing_hand:
Z/nZ を表す型として IntResidueClass というデータ型と、有限体を表す型クラスとして FiniteField 型クラスを作りました。
n が素数のときにZ/nZが有限体になることを次のようにしてプログラムにしました:writing_hand::scream_cat:

class FiniteField k where
  hoge :: k -> String

newtype IntResidueClass (n :: Nat) = MkIntResidueClass Integer deriving (Show)

instance (IsPrime p) => FiniteField (IntResidueClass p) where
  hoge _ = "hogehoge"


IsPrime は以下のように型族として定義しました。Natの型が素数になってるかどうかコンパイル時に判定させることができました:exploding_head:

type family (x :: Nat) % (y :: Nat) :: Nat  where
  x % y = Mod' x y (y <=? x)

type family Mod' (x :: Nat) (y :: Nat) (xGeqY :: Bool) :: Nat where
  Mod' x y 'True  = Mod' (x - y) y (y <=? (x - y))
  Mod' x y 'False = x

type IsPrime p = IsPrimeB p ~ 'True
  
type family IsPrimeB (p :: Nat) :: Bool where
  IsPrimeB 0 = 'False
  IsPrimeB 1 = 'False
  IsPrimeB 2 = 'True
  IsPrimeB p = IsPrimeB' p 3 (p % 2 == 0) (Not (3 ^ 2 <=? p))

type family IsPrimeB' (p :: Nat) (i :: Nat) (hasFactor :: Bool) (searchEnd :: Bool) where
  IsPrimeB' _ _ 'True _ = 'False
  IsPrimeB' _ _ _ 'True = 'True
  IsPrimeB' p i _ _     = IsPrimeB' p (i + 2) (p % i == 0) (Not ((i + 2) ^ 2 <=? p))


さらに、実行時のユーザの入力によって n を決めて IntResidueClass n 型の値を作り出すことは、以下のようにしてできました:oden:

main :: IO ()
main = do
  s <- getLine
  let i = read s :: Integer
  let sn = fromJust $ someNatVal i
  case sn of
    SomeNat p -> do
      let irc = mkIntResidueClassFromProxy p 0
      print irc 


このとき、 print $ hoge irc とするなどの、`FiniteField`クラスのメソッドを使うことができません:sob:
FiniteField クラスのインスタンスである IntResidueClass を実行時に作るにはどうすれば良いのでしょうか:sob::man-bowing:
@mashedhotate has joined the channel
KnownNat n からIntegerはいつでも変換できますが、どうしても値レベルの素数判定は使いたくないということですか?仮に型レベルの素数判定を使ったとしても、この場合結局実行時に評価することになって、性能はむしろ悪くなりそうですが
どういう状況なのかは分かりませんが,基本的なアイデアとしては, SomeNat と同じようにまず FiniteField の制約を持つ存在型で包んであげて, FiniteField のリフレクションでインスタンスを導出してあげれば良いです.ただ,Haskellはこの辺があまり柔軟にはできていないので,リフレクションに多少工夫が必要です.
そうですね。あとはGADTで型レベルのパターンマッチをするのもあると思います。GHCの型だけで数学を表現するのは大変で、たくさんの人が挫折してますね・・
どの道どのリフレクションを使うにしろ,何らかのユーザー保証は入ってくる(素数判定の結果がIsPrimeを満たすことを,GHCではなくユーザーが保証する. 型族の実装からの実行時動作を導出することは個人的には無理だと思っていますが,できるかもしれません できそうかもです.アイデアだけ次のコメントに書いておきました.)と思いますが,リフレクションの方法としては
1. IsPrime が1つのメソッドしか持たないなら https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection という方法があります.
2. もう一つは, Typeable () を利用して someNat で持ち上げた Nat の型情報を持ってくる方法があります
他にもいろいろありますが,代表的なのはこの辺ですかね?
あまり頭のいいことをしようと考えなければ,結構簡単にいけそうですね.とりあえず思いついた方法を書いてみました.参考にどうぞ
https://gist.github.com/mizunashi-mana/30bccdd729e1a069580ac17e9d0853f2
後,型族からの実装の抽出は,IsPrimeBが構造的帰納法などで停止することを証明して,KnownNat n => IsPrimeB n ’True \/ IsPrimeB n ’False であることを証明すれば,後はその証明を使って型レベルの’True/’Falseを値レベルのTrue/Falseに落としてTrueかどうか判定することでできそうな気がしました.まあ,ちょっとめんどそうなので,そっちの方は試してないです
今回は書き下してますが, とか使うともっとラクに書けるんじゃないかなと思います.
おお:heart_eyes:どうもありがとうございます:pray:
プログラムまで書いて頂いてものすごく参考になりそうです:man-bowing:
まだ全部理解できていないのですが、わからないことがあったらまた質問するかもしれないです:sweat_drops:
haskellの数値演算では型合わせが必須で、少しまともに書き始めると色々躓きまして、あちこち調べて整理しています。その中で過去の98のクラス階層図  おそらく最新と思われるものの間で違いがあります。具体的にはNumについていたEqやshowの型制約が外れているようなのですが、これは何故なのでしょう?
結構前に、 Num クラスに Eq, Show 制約は不要だからなくなったと記憶しています。 xuwei さんのブログ記事がありました: http://xuwei-k.hatenablog.com/entry/20120123/1327325922
http://downloads.haskell.org/~ghc/latest/docs/html/users_guide/bugs.html#numbers-basic-types-and-built-in-classes にも同じ話がありましたが、 やっぱり詳しい背景までは載ってませんね すみません、 :point_up: の記事でも軽く触れてますね。
推測ですが、単純に Eq であることと Show であることとは Num に本質的でないと判断したんではないでしょうか。
ありがとうございます。公式に外されたものなのですね。図の中で制約が外れた後も「All except~」とあるので、暗黙的に制約される何がしかの仕組みがあるのかと勘繰っていました。提案の中に書かれているように”意味がない”ということなのですね
引き続き、数値演算時の型変換の質問です。
これを見ながら色々考えていたのですが、`realToFrac`の使いどころが分からなくなりました。
整数型からの変換は`fromIntegral`一択。`Rational`へ・からの変換はそれぞれ専用関数があり、`Fractional`からの整数型への変換は何らかの切り捨て関数となると、`realToFrac`は`Fractional`間の変換時の使用に見えます。
ただ、 では、浮動小数点型の変換に`realToFrac`を使うのは問題があるので、専用関数を使え、とあります。(上表にはRWHの記述にくわえて、相互変換関数を追記してあります)
となると、`realToFrac`の使いどころがわからなくなりました。ネット等にあるサンプルは比較的単純で`realToFrac`を使わずとも他の関数で書いても同じ結果になりました。もしかしてcomplexあたりとの演算??分かれば単純なことな気がしていますが、思いつかなかったのでご教授いただけると嬉しいです
https://www.stackage.org/haddock/lts-10.5/base-4.10.1.0/Prelude.html#t:Fractional を見る限り、
お察しの通りComplexはRealじゃないかつFractionalである場合があるみたいですね。
ただ、実際のところ
realToFrac = fromRational . toRational

で定義される程度の、ユースケースの割にはシンプルな関数です(個人の感想です)。
歴史の闇の中でいろいろ仕様変更しているうちに要らないものができちゃった、なんてことは普通にあり得ますが。。。 :cold_sweat:
早々のお返事ありがとうございます。RWHには実際にはrealToFracではなく、fromRational.toRationalで書かれていますね。
いわゆる入門系の書籍やネットの記事等も比較的古めの情報が多いため、今ソースコードをみたときに事情が異なっているものが多いなあというのは昨日の例も含め、すごく感じています
:thinking_face: realToFrac を deprecate にした方がいいか議論した方がいいのだろうか。。。
今 RWH 読むならこちらも参考にどうぞ http://d.hatena.ne.jp/kazu-yamamoto/20140206/1391666962
質問です。
以下のコードはDataKinds+PolyKindsではコンパイルが通らず、TypeInTypeを有効にすると通ります。

{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}

import GHC.TypeLits

type S = Symbol

type family T :: Symbol -- OK
type family T2 :: Maybe Symbol -- OK
type family T3 :: Maybe S -- Error!


エラー内容

kind.hs:8:25: error:
    ? Type constructor ‘S’ cannot be used here
        (Perhaps you intended to use TypeInType)
    ? In the first argument of ‘Maybe’, namely ‘S’
      In the kind ‘Maybe S’


TypeInTypeの意味は「*のカインドを*とし、型と同様に扱えるようにする」との事ですが、上記のコードが通る事がそれとどのように関係しているのか理解できていません。
DataKinds+PolyKindsで上記のコードが通らないのはどのような制約によるもので、なぜTypeInTypeを指定するとそれが外れるのでしょうか。
(ぜんぜん詳しく無いですけど)
そもそも type alias の型では kind に昇格できないのではないですか?
type family T4 :: S -- Error!
最後の方に TypeInType について書いてありますね
https://haskell.jp/blog/posts/2017/13-about-kind-system-part2.html
僕も全然詳しくないですが,それは一重にDataKindsの型システムではtype aliasのpromotionが許可されていないけど,TypeInTypeの型システムでは許可されているからだと思いますね.GHCの現状のTypeInTypeの実装がどういう風になっているかはあまり知らないのですが,「*のカインドを*とする」のはinfiniteなtype hierarchyを許可することのように聞こえます
TypeInTypeの原論文のIntroductionがいちよ解になってる気がします.
http://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf
型の同値判定を種の同値判定に昇格するのが難しいと言ってますね.おそらくですが,この辺の兼ね合いでtype aliasを含めた型の同値判定を,既存の型システムで種レベルに昇格するのが難しかったのではないでしょうか?
数値の型について、もうひとつ。

皆さんは`Fracitonal‘ってどんな日本語をあてられますか?(日本語になんかしないよ、という意見は置いておいて)。
直訳は「分数」で手元にある虎本でも思い切り「分数」と訳されていますが、クラス間の関係から考えると「非整数」あたりが一番正確なのかな、と思っています。
「分数」だとサブクラスに√やpiや複素数があることと整合しない気がしまして・・

この流れでいうと`RealFrac`は非整数のうち実数のもの、`RealFloat`は浮動小数点の実数(`Floating`は複素数も含む)という理解で正しいでしょうか?
pi = pi / 1
だし、分数でもいいのでは?
pi や √ があるとおかしいのは有理数じゃない?
Oh…
Languages such as Coq and Agda avoid the : axiom because it introduces inconsistency, but that is not an issue here. The FC type language is already inconsistent in the sense that all kinds are inhabited.
なんですね,知りませんでした… 本当に文面通り*のカインドを*にするんですね…
無理数とは分数で表現できない数値(分子分母ともに整数である分数=有理数、以外の値)で、代表は2の平方根や円周率だと教わりました。分数で表現できないのが無理数なのに分数クラスっていうのはと思ったのですが、なるほどpi/1という捉え方も確かにありますね・・
無理数は 有理数 (分母と分子が整数の分数)で表現できない数だと思うよ
ぼくも専門ではないけど、分数はもっと一般化された概念なんじゃない?
上の記述、おかしいですね。分子分母ともに整数である分数=有理数で、それ以外が無理数。なので、よく「無理数は分数で表現できない数」といった説明がされています(ちょっと書き方直しました)
さらに`Rational`が`Ratio Integer`で(分母分子整数による分数)あることを考えると、やっぱり分数という日本語には個人的には違和感がありました
数学の話ですが、rational を有理数と訳したのは、誤りとだったと言われています。