問題タブ [mlton]

MLton のドキュメントによると:

標準 ML では、使用する前に型を定義する必要があります。【リンク】

すべての実装がこの要件を強制するわけではありません (たとえば、SML/NJ は強制しません) が、上記のリンクのページは、健全性のために必要になる理由 (実装が値の制限をどのように処理するかによって異なります) の良い例です。定義のコメントの一部と一致します。

私たちの定義では想定されていませんが、すべてのコンテキストC = T、U、EがE ⊆ Tという名前のプロパティを持つことが意図されています。したがって、 Tは大まかに、「生成された」すべての型名を含むと考えることができます。[…] もちろん、「生成された」ものについての発言は、意味規則に関して正確ではありません。しかし、次の正確な結果は簡単に実証できます。

S を文T , U , E ⊢句⇒ Aとし、 E ⊆ Tを tynamesとし、S' を S の証明に現れる文T ', U ', E ' ⊢句⇒ A ' とする。次に、 E ' ⊆ T 'も tynames します。

[21ページ]

しかし、私はこれに二重に混乱しています。

まず、上記の定理は後ろ向きに見えます。「Sの証明で発生する」というフレーズを正しく理解すると、これは（対比によって）「E ⊆ Tという名前の意図に違反するコンテキストがあると、後続のすべてのコンテキストもその意図に違反する」ことを意味するようです。それが本当だとしても、逆を主張する方がはるかに有用で意味があるように思われます。 "。いいえ？

第二に、MLton のステートメントもDefinitionのステートメントも、実際には推論規則 (またはそれに続く「さらなる制限」) によってサポートされているようには見えません。いくつかの推論規則には、副条件として「tynames τ ⊆ T of C」または「tynames VE ⊆ T of C」がありますが、このプログラムにはこれらの規則は必要ありません (上記のリンクのドキュメントに記載されています)。

(具体的には、規則 (4) はlet、規則 (14) は=>、規則 (26) は と関係recがあります。このプログラムでは、これらのいずれも使用されていません。)

そして、別の方向から来ると、宣言をカバーするルール (17) は、生成された型名がCのTにdatatypeないことだけを要求します。したがって、既存の値環境で使用される型名の生成を妨げません (ただし、VE ⊆ TのCという名前が既に真である場合を除きます)。

ここにはかなり基本的なものが欠けているように感じますが、それが何であるかはわかりません!

私が想像できる唯一の方法は Emscripten を使用することですが、MLTon には LLVM バックエンドがありません。なんとなく可能ですか？

I'm trying to build the sml3d from the SVN source (is there an another way?).

First, checked out the source with the following command like below:

Then, I read sml3d/README 'BUILDING FROM SVN' section and tried like ...

At this point, I got these many errors...

Next, I guess the correct building protocol like below:

But I got not-exists and Undefined errors yet:

How to build sml3d correctly ?

environment

I use runtime/systems...

• smlnj 110.77
• mlton 20130715
• linux x86

次のエントリを 1 と前のエントリに設定して、配列を反復処理する次のベンチマークがあります。数が特定の上限を超えた場合は、エントリをゼロに設定して続行します。最後に、配列内のエントリを合計します。

質問 : PolyML のベンチマーク結果を改善するにはどうすればよいですか?

Ubuntu x86-64 での時間は次のとおりです。

mlton は C コード (5.2s) とほぼ同じ速度で実行できますが、最新バージョンの gcc を使用して Windows 7 でシームレスにビルドできる PolyML に特に興味があります。(MSYS / MSYS2 および mingw gcc コンパイラを使用した Windows 7 での polyML のビルド手順については、http://lists.inf.ed.ac.uk/pipermail/polyml/2015-August/001593.html を参照してください)

Windows 7 では、最新バージョンの gcc を使用して mlton の最新バージョンをビルドする際に問題が発生しました ( https://github.com/MLton/mlton/issues/61#issuecomment-50982499と同様の問題 ) 。

SML コードは次のとおりです。

C++ コードは次のとおりです。

Standard ML でのプログラムのコンパイルに問題があります。

このプログラムは完全に動作し、ローカル マシンで完全にコンパイルされます。しかし、クラスター上の別の場所で実行するために、静的にコンパイルできるようにしたいと考えています。

プログラムをコンパイルするために使用しているコマンドは次のとおりです。

ファイルは次のsrc/spartacus.mlbとおりです。

コンパイルの最後の部分の StackTrace は次のとおりです。

MLTonのドキュメントを確認しましたが、静的コンパイルに関する情報は見当たりませんでした:/

誰かがそれを行う方法を知っていれば、それは私を大いに助けます! 前もって感謝します、

よろしくお願いします;

編集

クラスターで、./spartacus を実行しようとすると

REAL シグネチャで説明されているように、SML で定義されている実数型は等価型ではないため、次の式は還元されません。

ただし、実数を含むデータ型とリストも等しくなくなるため、これは便利ではありません。実数もほぼ考慮できるように、ポリモーフィックな等価性をオーバーロードする必要があり=ます。Real.==

それは可能ですか？

編集：より明確にするために質問を編集しました

8、16、32 ビット ワードを 64 ビット ワードに変換するポリモーフィック関数を作成したいと思います。どうすればいいですか？

更新1

基本ライブラリでは、すべての単語構造には関数がtoLargeあり、 とfromLargeの間で変換しLargeWordます。これは、私が理解している限り、Word32 の同義語です。

更新2

仕様によると、ワード サイズは 2 の累乗でなければなりませんが、SML/NJ では

PolyML にいる間

それはどうですか？Word.wordSize2 のべき乗でないのはなぜですか? Wordまた、これらの SML 実装で表現が異なるのはなぜですか?

更新3

実際、(<<) 演算子を使用して小さな単語を大きな単語に「昇格」させたいのですが、その方法がわかりません。

更新4

WordアーキテクチャにLargeWord依存し、機械語を表すようです。SML/NJ は 64 ビット アーキテクチャをサポートしていないため、ワード サイズが異なります。