3

このブログ投稿をフォローしています: http://semantic-domain.blogspot.com/2012/12/total-functional-programming-in-partial.html

これは、 System T (単純な完全関数型言語)用の小さな OCaml コンパイラ プログラムを示しています。

パイプライン全体が (Camlp4 メタプログラミングを介して) OCaml 構文を使用して、それらを OCaml AST に変換し、SystemT ラムダ計算 (参照: module Term) に変換し、最後に SystemT Combinator 計算 (参照: module Goedel) に変換します。最後のステップも OCaml メタプログラミングAst.exprタイプでラップされます。

Template Haskell を使用せずに Haskell に変換しようとしています。

SystemT Combinator フォームについては、次のように記述しました。

{-# LANGUAGE GADTs #-}

data TNat = Zero | Succ TNat

data THom a b where
  Id :: THom a a
  Unit :: THom a ()
  ZeroH :: THom () TNat
  SuccH :: THom TNat TNat
  Compose :: THom a b -> THom b c -> THom a c
  Pair :: THom a b -> THom a c -> THom a (b, c)
  Fst :: THom (a, b) a
  Snd :: THom (a, b) b
  Curry :: THom (a, b) c -> THom a (b -> c)
  Eval :: THom ((a -> b), a) b -- (A = B) * A -> B
  Iter :: THom a b -> THom (a, b) b -> THom (a, TNat) b

Composeは順合成であり、 とは異なることに注意してください(.)。

SystemT ラムダ計算から SystemT コンビネータ計算Elaborate.synthへの変換中に、関数は SystemT ラムダ計算変数を一連の合成射影式 (De Brujin Indices に関連) に変換しようとします。これは、コンビネータ計算に変数/変数名がないためです。Elaborate.lookupこれは、 関数を使用する で行われQuote.findます。

問題は、コンビネータ計算を GADT としてエンコードすることTHom a bです。関数の翻訳Quote.find:

  let rec find x  = function
    | [] -> raise Not_found
    | (x', t) :: ctx' when x = x' -> <:expr< Goedel.snd >> 
    | (x', t) :: ctx' -> <:expr< Goedel.compose Goedel.fst $find x ctx'$ >>

Haskellに：

find :: TVar -> Context -> _
find tvar [] = error "Not Found"
find tvar ((tvar', ttype):ctx)
  | tvar == tvar' = Snd
  | otherwise     = Compose Fst (find tvar ctx)

無限型エラーになります。

• Occurs check: cannot construct the infinite type: a ~ (a, c)
  Expected type: THom (a, c) c
    Actual type: THom ((a, c), c) c

この問題は、GADTComposeで andFstとSndfromを使用するとTHom a b、型シグネチャが無限に変化する可能性があるという事実から生じます。

Ast.exprこの記事では、 OCamlを使用して基になる式をラップしているように見えるため、この問題はありません。

Haskellで解決する方法がわかりません。次のような存在量化型を使用する必要がありますか

data TExpr = forall a b. TExpr (THom a b)

Fixまたは、無限型の問題を適応させるためのある種の型レベル。findただし、これがor関数をどのように変更するかはわかりませんlookup。

4

1 に答える 1

2

この問題を解決するために考えられる設計には 3 つのまったく異なるファミリがあるため、この答えは少し大まかにする必要があります。あなたがしていることは、アプローチ 3 に近いように見えますが、アプローチは複雑になる順に並べられています。

元の投稿のアプローチ

元の投稿を翻訳するには、テンプレート Haskell と部分性が必要です。元の投稿と同じように、この問題を回避して、を表す somefindを返します。元の投稿と同じように、すべての Template Haskell 関数の出力を型チェックすると、元のコードの型エラーが検出されます。したがって、型エラーは実行前にキャッチされますが、マクロが不適切な型の式を出力するケースを見つけるためにテストを作成する必要があります。複雑さの大幅な増加を犠牲にして、より強力な保証を与えることができます。Q.ExpHom a b

入力と出力の依存タイピング/GADT

投稿から逸脱したい場合、代替の 1 つは、全体で「依存型入力」を使用し、入力を依存型型にすることです。私はこの用語を大まかに使用して、実際に依存型付けされた言語、実際の依存型 Haskell (それが着陸したとき)、および今日の Haskell で依存型型付けを偽装する方法 (GADT、シングルトンなどを介して) の両方を含めます。ただし、独自の型チェッカーを記述して、使用する型システムを選択することはできません。通常、単純型付けされたラムダ計算を埋め込むことになり、特定の型で項を生成できる多態的な Haskell 関数を介して多態性をシミュレートできます。これは依存型言語ではより簡単ですが、Haskell ではまったく可能です。

しかし正直なところ、この道では、次のような高次の抽象構文と Haskell 関数を使用する方が簡単です。

data Exp a where
  Abs :: (Exp a -> Exp b) -> Exp (a -> b)
  App :: Exp (a -> b) -> Exp a -> Exp b
  Var :: String -> Exp a —- only use for free variables
exampleId :: Exp (a -> a)
exampleId = Abs (\x -> x)

このアプローチを使用できる場合 (ここでは詳細は省略します)、複雑さを抑えた GADT から高い保証が得られます。ただし、このアプローチは多くのシナリオでは柔軟性がありません。たとえば、型付けコンテキストは Haskell コンパイラにのみ表示され、型や用語には表示されないためです。

型付けされていない用語から型付けされた用語へ

3 番目のオプションは、依存型付けを行うことであり、プログラムで弱く型付けされた入力を強く型付けされた出力に変換します。この場合、タイプチェッカーは全体的に、何らかのタイプのExpr用語を GADT TExp gamma t、Hom a bまたはそのような用語に変換します。gammaand t(またはaand ) が何であるかを静的に知らないためb、実際にはある種の存在が必要になります。

しかし、単純な存在論は弱すぎます。より大きな適切に型付けされた式を構築するには、生成された型がそれを許可することを確認する必要があります。たとえばTExpr、式を含むComposeを 2 つの小さいから作成するTExprには、(実行時に) それらの型が一致することを確認する必要があります。そして、単純な実存主義では、できません。したがって、値レベルでも型の表現が必要になります。

戻り値の型で非表示の型変数を公開したり、それらを投影したりすることはできないため (従属レコード/シグマ型とは異なります)、さらに存在論を扱うのは面倒です (いつものように)。正直なところ、これが最終的に機能するかどうかは完全にはわかりません。これは、Haskell で可能な部分的なスケッチですfind。

data Type t where
  VNat :: Type Nat
  VString :: Type String
  VArrow :: Type a -> Type b -> Type (a -> b)
  VPair :: Type a -> Type b -> Type (a, b) 
  VUnit :: Type ()
data SomeType = forall t. SomeType (Type t)
data SomeHom = forall a b. SomeHom (Type a) (Type b) (THom a b)

type Context = [(TVar, SomeType)] 
getType :: Context -> SomeType
getType [] = SomeType VUnit 
getType ((_, SomeType ttyp) :: gamma) =  
   case getType gamma of
       SomeType ctxT -> SomeType (VPair ttyp
find :: TVar -> Context -> SomeHom 
find tvar ((tvar’, ttyp) :: gamma)
   | tvar == tvar’ =
       case (ttyp, getType gamma) of
         (SomeType t, SomeType ctxT) ->
          SomeHom (VPair t ctxT) t Fst
于 2018-11-17T23:39:23.007 に答える