Idris dependent records with interface constraint on Type Constructor parameter

4
votes

Is it possible to have interface constraints on a parameter to a type constructor of a dependent record in idris? Say I have an interface Show : Type -> Type. Now I need to place a constraint on the following dependent record:

record Source s where
   constructor MkSource
   initial : s

I need to place a constraint on the parameter sso that it should always be a instance of Show. How to achieve this?

1
idristype-constraints
By "always an instance of Show" do you mean there should exist a witness ss : Show s ? If yes, why not just add another field to Source of type Show s? – Cactus
Can you please include the actual definition of the Show interface in your question (ie using the keywords interface and where). – Philip Dorrell

1 Answers

2
votes

Idris is under heavy development but according to this recent email to the idris group the record syntax does currently not support constraining types with an interface:

https://groups.google.com/forum/#!topic/idris-lang/HMeTylslyFc

You will need to use data type syntax instead, e.g. 

module Main

data Source: Type -> Type where
    MkSource: Show s => s -> Source s


x: Source Int
x = MkSource 3

showSource: Source s -> String
showSource  (MkSource x) = show $ x

testMe: (showSource $ Main.x = "3")
testMe = Refl