Приложение видимого типа в Haskell: как связать тип - PullRequest
Новая
       40

Приложение видимого типа в Haskell: как связать тип

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

В приложении видимого типа можно указать, для какого типа мы «вызываем» полиморфное значение.

Это позволяет удалять такие значения, как Proxy :: Proxy s, только для привязки типа s, когда мы являемся пользователем.мы просто пишем myPolyValue @ s

Но если мы строим полиморфное значение, есть ли способ связать тип, к которому мы обращаемся, кроме аргумента типа Proxy s?

Пример Я использую VisibleTypeApplication, чтобы вызвать полиморфный тип, но я понятия не имею, как связать тип, к которому я был привязан, за исключением аргумента Proxy s:

#!/usr/bin/env stack
-- stack --resolver nightly-2018-12-12 script --package base-unicode-symbols --package unicode-prelude --package constraints
{-# LANGUAGE AllowAmbiguousTypes,GeneralizedNewtypeDeriving  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies, KindSignatures #-}
{-# LANGUAGE FlexibleContexts , TypeApplications #-}
{-# LANGUAGE InstanceSigs , FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses , ScopedTypeVariables #-}
{-# LANGUAGE GADTs , MultiParamTypeClasses     #-}
{-# LANGUAGE RankNTypes , TypeOperators             #-}
{-# LANGUAGE UnicodeSyntax,DataKinds              #-}

module ImplicitConfigurationFirstPart where

import Data.Proxy

data KNat where
  Zero :: KNat
  Twice :: KNat -> KNat
  Succ :: KNat -> KNat
  Pred :: KNat -> KNat

class ReflectNum (s :: KNat) where reflectNum ∷ Num a ⇒ Proxy s -> a
instance                ReflectNum  'Zero      where reflectNum _ = 0
instance ReflectNum s ⇒ ReflectNum ('Pred  s) where reflectNum _ = (reflectNum (Proxy @ s)) - 1
instance ReflectNum s ⇒ ReflectNum ('Succ  s) where reflectNum _ = (reflectNum (Proxy @ s)) + 1
instance ReflectNum s ⇒ ReflectNum ('Twice s) where reflectNum _ = (reflectNum (Proxy @ s)) * 2

reifyIntegral ∷ (Integral a) ⇒ a → (∀ (s :: KNat). ReflectNum s ⇒ Proxy s -> w) → w
reifyIntegral i k = case quotRem i 2 of
  (0,0)  → k $ Proxy @ 'Zero
  (j,0)  → reifyIntegral j (\(p :: Proxy s) -> let n = reflectNum p in
                                               k $ Proxy @ ('Twice s) )
  (j,1)  → reifyIntegral j (\(_ :: Proxy s) -> k $ Proxy @ ('Succ('Twice s)))
  (j,-1) → reifyIntegral j (\(_ :: Proxy s) -> k $ Proxy @ ('Pred('Twice s)))

Попытка1 В этом примере первый случай с индексом Zero работает нормально.

Но второй не может доказать, что 'Twice s является частью ReflectNum.Тем не менее, как s, при котором будет применяться k1, проверяется ReflectNum, так что 'Twice s проверяет его и k, будучи полиморфным в s, при условии, что у нас есть доказательство ReflectNum s,можно назвать. 

{-# LANGUAGE AllowAmbiguousTypes,GeneralizedNewtypeDeriving  #-}
{-# LANGUAGE  TypeFamilies, KindSignatures, FlexibleContexts #-}
{-# LANGUAGE TypeApplications, FunctionalDependencies, MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables , GADTs, MultiParamTypeClasses, RankNTypes                #-}
{-# LANGUAGE TypeOperators, UnicodeSyntax, DataKinds              #-}
{-# LANGUAGE UndecidableSuperClasses    #-}
module ImplicitConfigurationFirstPart where

import Data.Proxy

data KNat where
  Zero :: KNat
  Twice :: KNat -> KNat

class ReflectNum (s :: KNat) where reflectNum ∷ Num a ⇒ Proxy s -> a
instance                ReflectNum  'Zero      where reflectNum _ = 0
instance ReflectNum s ⇒ ReflectNum ('Twice s)  where reflectNum _ = (reflectNum (Proxy @ s)) * 2

reifyIntegral2 ∷ forall a w. (Integral a) ⇒ a → (∀ (s :: KNat). ReflectNum s ⇒ w) → w
reifyIntegral2 i k = case quotRem i 2 of
  (0,0)  → k @ 'Zero
  (j,0)  → reifyIntegral2 j k1

  where k1 :: forall (s :: KNat). ReflectNum s ⇒ w
        k1 = k @ ('Twice s)

1 Ответ

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

Но если мы строим полиморфное значение, есть ли способ связать тип, к которому мы призываем, кроме аргумента типа Proxy s?

Если я правильно понимаю, вы имеете в виду, что вы хотите определить полиморфную привязку, которая принимает аргумент типа, который предназначен для предоставления с использованием приложения видимого типа.Ответом на этот вопрос является использование forall.

Если у вас есть какая-то функция f, написанная с использованием Proxy s, такая как 

f :: Proxy s -> X -> Y

, тогда вы можете исключить Proxy аргумент, включив AllowAmbiguousTypes и ScopedTypeVariables и используя вместо этого явный forall: 

{-# LANGUAGE AllowAmbiguousTypes, ScopedTypeVariables #-}
f :: forall s. X -> Y

Переменная типа s будет связана в теле f.

...