1
私は最近算術計算のためのコンパイル時の科学単位を得るためにDataKindsを使いこなし始めました。私は多かれ少なかれ私が欲しいものをする方法を考え出したが、私はそれがもっときれいになるかもしれないように感じる。ハスケルのデータ型で整数リテラルと算術を使用する方法
ネガティブ（m^-1）の可能性がある整数が必要なので、ナチュラルではなく整数を使用することに決めました。しかし、あなたが:k 5をしたときにそれはあなたにGHC.Types.Natを与え、私のニーズに合っていません。私は代わりに私の独自のカスタム代数整数型を作成しました。それと共に使用する加算および減算タイプファミリの定義だけでなく、
しかし、これはすべて間接的なようですが、タイプファミリー内でコンパイル時にデータを操作するための既存の関数をすべて直接使用することはできないのです。
基本的に私は次のように、本質的に自動的に生成されるようにしたい：
type family (a :: Int) + (b :: Int) :: Int where
-- Should be automatically derivable from (+) applied to Int
がいる可能性があり、そうでない場合は、なぜありませんか？
また、タイプからランタイム値を取得する簡単な方法はありますか？具体的には、これらすべてのタイプのインスタンスをShowと書くときは、基本的にユニットの組み合わせを表すファントムタイプをプルして文字列に変換したいだけです。私はこれをやっていると考えることができるすべての方法は本当に冗長に思える。
これは現在のHaskellではできないと思います。型ファミリ定義では、値式（型を持つ）、型式（型を持つ）のみを使用することはできません。したがって、私は現在、 '（+）'の値レベルの定義を参照する方法がないと信じています。 – chi
あなたは[Dimensional]（https://github.com/bjornbm/dimensional）に精通していますか？ –
"既存のすべての関数を直接使うことができないのは正当な理由ではありません" - なぜなら、Haskellは依存型言語ではないからです。値と型の間には分離があります。つまり、2つのレベル間でコードを複製し、シングルトン値のような面倒なハックを使用する必要があります。 [ハスケルのデザイナーはその制限を解除する作業に苦労している]（http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis-draft.pdf）;その間、AgdaやIdrisのような実際に依存型言語を使うことを検討することができます。 –