CODEWITHSUNDEEP
idristype-constraints
Aravindh S
Aravindh S

Reputation: 1245

Idris dependent records with interface constraint on Type Constructor parameter

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?

Upvotes: 4

Views: 513

Answers (2)

Janus Troelsen
Janus Troelsen

Reputation: 21270

You can do it like this:

record a {auto eq : Eq a} where
  constructor MkThing
  target : Int
  value : a

Source: Discord

Upvotes: 2

Markus
Markus

Reputation: 1303

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

Upvotes: 2

Related Questions