Ограничение аргумента функции в интерфейсе

Каков синтаксис для ограничения аргумента функции в интерфейсе, который принимает функцию? Я попытался:

interface Num a => Color (f : a -> Type) where
     defs...

Но там написано Name a is not bound in interface...


idris
person ScarletAmaranth    schedule 22.04.2016    source источник

Ответы (1)


arrow_upward
5
arrow_downward

Ваш interface на самом деле имеет два параметра: a и f. Но f должно быть достаточно, чтобы выбрать implementation:

interface Num a => Color (a : Type) (f : a -> Type) | f where

f здесь называется определяющим параметром.

Вот бессмысленный полный пример:

import Data.Fin

interface Num a => Color (a : Type) (f : a -> Type) | f where
  foo : (x : a) -> f (1 + x)

Color Nat Fin where
  foo _ = FZ

x : Fin 6
x = foo {f = Fin} 5
person Cactus    schedule 23.04.2016
comment
Ооо, у меня был интерфейс с двумя параметрами, но я не понимал, что могу использовать | f, чтобы заставить принимать решение только один, это отлично. - person ScarletAmaranth; 23.04.2016