我怎樣才能多型地解釋一個類似Arrow的GADTDSL？

TL;DR:我如何為我的LangGADT撰寫解釋器（run :: Lang a b -> whatever）？

我有一個DSL:

data Lang a b where
  F :: Lang x y
  G :: Lang x y

我想建立這樣的程式：

prog :: Lang a b
prog = G . F.

并且任意地解釋它們，其中F和G的替換可以是任何函式，只要它們的型別組成正確。

-- run ~= ( 1) . fst
run :: Lang a b -> （(Int, b) -> Int)
run F = fst
run G = ( 1) -- 錯誤：無法與Int型別（Int, b）匹配。

解釋是我的大問題。我怎樣才能寫出這樣的函式：

run :: Lang a b -> whatever --例如重復使用變數。 run :: Lang a b -> （a -> IO b)

我在我的語言中加入了組成的概念：

我的語言中加入了組成的概念。

data Lang a b where
  ...

  Lift :: (a -> b) -> Lang a b
  Comp :: Lang b c -> Lang a b -> Lang a c

instance C.Category Lang where
  id = Lift id
  (.) = Comp 

這使我能夠構建程式，但不能解釋它們。我理解編譯器對我的錯誤，當我試圖將一個特定的術語實體化為某種型別，而這個型別不是整個run fn的型別。

這似乎有點像Free的方法，也許是一個索引的Free？與此相關，這是我真正問題的一個簡化版本，它主要使用Arrows，但是，我認為這個簡化的表述概括了我的問題。

這里有一個可運行的測驗環境：

{-# LANGUAGE GADTs #-}

module T15_GADT_Lang where

import qualified Control.Category as C

------------------------------
-- * My Lang

data Lang a b where
  -- | DSL
  F :: Lang x y
  G :: Lang x y

  -- | 組成。
  Lift :: (a -> b) -> Lang a b
  Comp :: Lang b c -> Lang a b -> Lang a c

instance C.Category Lang where
  id = Lift id
  (.) = Comp[/span]>

------------------------------
-- *程式A可以用2種不同的方式來解釋。

progA :: Lang a b
progA = F

runA1 :: Lang a b -> （Int -> String)
runA1 F x = show x <> "!

runA2 :: Lang a b -> ([Double] -> String)
runA2 F x = show x <> "!

progAWorksNicely =do
  putStrLn $ runA1 progA  123
  putStrLn $ runA2 progA [1.3]


------------------------------
-- * 程式B，我不能獨立地解釋臨時函式。

progB :: Lang a b
progB = G C. F.

--|獲得fst并遞增。
runB1 :: Lang a b -> （(Int, b) -> Int)
runB1 F = fst
runB1 G = ( 1) -- 錯誤：無法與Int型別（Int, b）匹配。

-- | 獲取頭部并復制它。
runB2 :: Lang a b -> ([a] -> (a, a))
runB2 F xs = head xs --你給了一個`a`，但應該是`(a,a)`。
runB2 G x = (x, x)

uj5u.com熱心網友回復：

你可以只用Lift和Comp來寫這些不同的解釋，但是如何將F解釋為fst和head都有意義，就不太明顯了

-- > run (Lift (x -> show x <> "!") ) 1
-- "1!"
-- > run (Lift (x -> show x <> "!") [pi,pi]
-- "[3.141592653589793,3.141592653589793]!"
-- > run (Lift (1  ) `Comp` Lift fst) (100, "ok")
-- 101
-- dup a = （a, a）
-- >> run (Lift dup `Comp` Lift head) [1,2,3] 
-- (1, 1)
運行 :: Lang a b -> (a -> b)
run (Comp f g) = run f . run g
run (Lift f) = f

F和G的問題是，它們的索引是完全普遍量化的，這意味著用它們進行組合還不如不型別化，因為任何輸入和任何輸出都是有效的！

如果你想要型別安全的 G 的組合。F的解釋必須以某種方式連接到這些型別，因此您必須為Lang提供索引，以統一這兩種用法

run F = fst :: (a, b) -> a
run G = ( ) 1 ::           Int -> Int

run F = head :: [a] -> a
run G = dup :: a -> (a, a)

在Lift的情況下，輸入和輸出型別清楚地反映在索引中。它們中的每一個都可以被做成一個獨立的建構式，并以不同的方式進行索引。

Lift (x -> show x <> "！") :: Lang Int String
Lift (x -> show x <> "！") :: Lang [Double] String
Lift fst :: Lang (a, b) a
Lift (1  ) :: Lang Int Int Int
Lift head :: Lang [a] a
Lift dup :: Lang a (a, a)

如果你想把F解釋為fst，把G解釋為( 1)，你就有型別匹配

type Lang : 。Cat Type>
data Lang a b where
  One :: Lang (a, b) a
  Plus1 :: Lang Int Int >。
  ..

-- > run (Plus1 . One) (100, 200)
-- 101.
運行 :: Lang a b -> (a -> b)
run One = fst
運行 Plus1 = ( ) 1。
..

你可以類似地解釋為一個IO-kleisli箭頭

切線

你也可以通過將建構式抽象為一個型別類的方法來解釋它，并通過該類的約束來解釋它

我想目的是把Lift id當作Comp的身份，就像類別操作那樣。語言可以表達為"免費的Category"

type Langc :: Cat Type -> Constraint 
class Category cat => Langc cat where
 one :: cat (a, b) a
 plus1 :: cat Int Int
 lift :: (a -> b) -> cat a b

run :: Lang a b -> (forall lang. Langc lang => lang a b)
run = case.
 One -> one
 Plus1 -> plus1
 Lift f -> lift f
 Comp f g -> run f . run g

或者一個自由的Arrow，它有arr :: Arrow arr => (a -> b) -> arr a b

type Langc :: Cat Type -> Constraint 
class Arrow arr => Langc arr where
 one :: cat (a, b) a
 plus1 :: cat Int Int

run :: Lang a b -> (forall lang. Langc lang => lang a b)
run = case.
 One -> one
 Plus1 -> plus1
 Lift f -> arr f
 Comp f g -> run f . run g

這可以在Langc (->)和Langc (Kleisli IO)進行解釋。

事實上，你可以跳過 "初始 "的Lang編碼，將其定義為 "最終"

type Lang :: Cat Type>
type Lang a b = (for all lang. Langc lang => lang a b) 

f :: Lang (Int, a) Int
f = one >> > plus1

-- > run f (100, "ok")
-- 101
run :: Lang a b -> (a -> b) -- requires: instance Langc (-> )
run lang = lang

標籤：

上一篇：Haskell串列上的遞回如何作業

下一篇：使用>>=表達基本的數字決議器