CODEWITHSUNDEEP
haskellclash
error_null_pointer
error_null_pointer

Reputation: 455

Removing the type constraint on a type to a value that satisfies the constraints. I.e. Num a => a to just Int

I am using a system called CLaSH. For those who are not familiar it is designed in a way that allows you to develop for FPGAs using Haskell.

I am trying to create an Unsigned value. 

Defined at: https://hackage.haskell.org/package/clash-prelude-0.10.11/docs/src/CLaSH-Sized-Internal-Unsigned.html#Unsigned

Something like: 

2 :: Unsigned 3

works. I want to be able to do something like:

x = 3

2::Unsigned x

But I get the error:

No instance for (KnownNat x1) arising from the literal `2'

 

Possible fix:

 add (KnownNat x1) to the context of

 an expression type signature: Unsigned x1

 In the expression: 2 :: Unsigned x

 In an equation for `it': it = 2 :: Unsigned x

I then tried "fromInteger#" defined in the same file. 

let y=fromInteger# x

which returns the type

y :: KnownNat n => Unsigned n

With that 'y' I can give it a size by adding an unsigned with a specified size. 

y + (2 :: Unsigned 3)

which gives a  5

it :: Unsigned 3

How do I get a something like 

2::Unsigned x

If I can't do this, why can't I?

EDIT: It is possible to do what I needed using template Haskell. See code below and link to CLaSH group explanation

https://groups.google.com/forum/#!topic/clash-language/uPjt8i0lF0M . 

What I wanted I could accomplish at compile time. Runtime would be impossible.

Upvotes: 3

Views: 155

Answers (1)

hao
hao

Reputation: 10228

If I understand you correctly, you want to be able to reference variables as type-level naturals in your type signatures. For this you have to declare x as a type (type or data) rather than a value. It is this distinction between values and types that separates Haskell from the older stock of dependently-typed languages, where you would be able to freely reference declarations in types without worrying about the differences between values and types. So, try making your code look something like this:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

module Lib where

import Data.Proxy
import GHC.TypeLits

data Unsigned (a :: Nat)
type X = 2

main :: IO ()
main =
  print (Proxy :: Proxy (Unsigned X))

I fear that I do not know anything about Clash, however, so perhaps I do not have the whole picture.

Upvotes: 4

Related Questions