Связывание типа с `Proxy s` против связывания типа с forall - PullRequest
Новая
       35

Связывание типа с `Proxy s` против связывания типа с forall

0 голосов
/ 13 декабря 2018

в следующем примере мне непонятно, почему toto потерпит неудачу, а tata сработает.

Есть ли какое-либо объяснение этому? 

{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE  TypeFamilies, KindSignatures, FlexibleContexts #-}
{-# LANGUAGE TypeApplications, FunctionalDependencies, MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables , GADTs, MultiParamTypeClasses, RankNTypes                #-}
{-# LANGUAGE TypeOperators, UnicodeSyntax, DataKinds              #-}

import Data.Proxy

data KNat where
class ReflectNum (s :: KNat) where

toto ∷ (∀ (s :: KNat). ReflectNum s ⇒ Int) → Int
toto k = toto k

tata ∷ (∀ (s :: KNat). ReflectNum s ⇒ Proxy s -> Int) → Int
tata k = tata (\(p :: Proxy s) -> k p)

Ошибка: 

SO.hs:14:15: error:
    • Could not deduce (ReflectNum s0) arising from a use of ‘k’
      from the context: ReflectNum s
        bound by a type expected by the context:
                   forall (s :: KNat). ReflectNum s => Int
        at SO.hs:14:10-15
      The type variable ‘s0’ is ambiguous
    • In the first argument of ‘toto’, namely ‘k’
      In the expression: toto k
      In an equation for ‘toto’: toto k = toto k
   |
14 | toto k = toto k
   |               ^

1 Ответ

0 голосов
/ 13 декабря 2018

Это известное ограничение реализации GHC приложения видимого типа.В частности, Proxy иногда все еще необходим для того, чтобы позволить аргументу функции более высокого ранга (например, вашей функции toto) получить доступ к переменной типа.

Существует предложение GHC добавитьРешение этой проблемы, в виде привязок переменных типа в лямбда-выражениях .Используя синтаксис предложения, ваша функция toto может быть записана как 

toto k = toto (\@s -> k @s)

для локального связывания переменной s.К сожалению, это предложение еще не было реализовано.

В то же время, для таких функций более высокого ранга, я думаю, вам просто нужно использовать Proxy.К сожалению.

...