8

次のコードがあり、これを型チェックに失敗させたい:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

import Control.Lens

data GADT e a where
  One :: Greet e => String -> GADT e String
  Two :: Increment e => Int -> GADT e Int

class Greet a where
  _Greet :: Prism' a String

class Increment a where
  _Increment :: Prism' a Int

instance Greet (Either String Int) where
  _Greet = _Left

instance Increment (Either String Int) where
  _Increment = _Right

run :: GADT e a -> Either String Int
run = go
  where
  go (One x) = review _Greet x
  go (Two x) = review _Greet "Hello"

アイデアは、GADT の各エントリに関連するエラーがあり、それをPrismより大きな構造にモデル化するというものです。この GADT を「解釈」するときe、これらすべてのインスタンスを持つ具体的な型を提供しますPrism。ただし、個々のケースごとに、コンストラクターの関連付けられたコンテキストで宣言されていないインスタンスを使用できるようにしたくありません。

上記のコードはエラーになるはずです。なぜなら、でパターン マッチを行うと、Twoしか使用できないことを学習するはずIncrement eですが、 を使用しているからですGreet。これが機能する理由がわかります-Either String IntのインスタンスがあるためGreet、すべてがチェックアウトされます。

これを修正する最善の方法が何であるかはわかりません。からの含意を使用できるData.Constraintか、またはより高いランクの型でトリックが存在する可能性があります。

何か案は？

4

1 に答える 1

7

問題は、最終的な結果の型を修正しているため、インスタンスが存在し、型チェッカーがそれを見つけることができることです。

次のようなものを試してください：

run :: GADT e a -> e

結果の型はインスタンスを選択できずreview、パラメトリック性が不変条件を強制します。

于 2014-04-29T13:19:44.027 に答える