msakai
ExplicitForAll の方が ScopedTypeVariables よりも導入が後だった気がする。
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
GHC.TypeLits の someNatVal 関数などを使えばできるとおもうのですが、この時作られる型を自作の型クラスのインスタンスに限定するにはどのようにすればいいのでしょうか?:sob::sob::innocent:IntResidueClass というデータ型と、有限体を表す型クラスとして FiniteField 型クラスを作りました。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))
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:SomeNat と同じようにまず FiniteField の制約を持つ存在型で包んであげて， FiniteField のリフレクションでインスタンスを導出してあげれば良いです．ただ，Haskellはこの辺があまり柔軟にはできていないので，リフレクションに多少工夫が必要です．IsPrime が1つのメソッドしか持たないなら https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection という方法があります．Typeable (someNat で持ち上げた Nat の型情報を持ってくる方法がありますEq であることと Show であることとは Num に本質的でないと判断したんではないでしょうか。realToFrac = fromRational . toRational
realToFrac を deprecate にした方がいいか議論した方がいいのだろうか。。。
{-# 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’
type family T4 :: S -- Error!
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.なんですね，知りませんでした… 本当に文面通り*のカインドを*にするんですね…